Big operators for NatAntidiagonal

This file contains theorems relevant to big operators over Finset.NatAntidiagonal.

theorem Finset.Nat.prod_antidiagonal_succ {M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : (Finset.prod (Finset.antidiagonal (n + 1)) fun (p : ℕ × ℕ) => f p) = f (0, n + 1) * Finset.prod (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f (p.1 + 1, p.2)

theorem Finset.Nat.sum_antidiagonal_succ {N : Type u_2} [AddCommMonoid N] {n : ℕ} {f : ℕ × ℕ → N} : (Finset.sum (Finset.antidiagonal (n + 1)) fun (p : ℕ × ℕ) => f p) = f (0, n + 1) + Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f (p.1 + 1, p.2)

theorem Finset.Nat.sum_antidiagonal_swap {M : Type u_1} [AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : (Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f (Prod.swap p)) = Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f p

theorem Finset.Nat.prod_antidiagonal_swap {M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : (Finset.prod (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f (Prod.swap p)) = Finset.prod (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f p

theorem Finset.Nat.prod_antidiagonal_succ' {M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : (Finset.prod (Finset.antidiagonal (n + 1)) fun (p : ℕ × ℕ) => f p) = f (n + 1, 0) * Finset.prod (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f (p.1, p.2 + 1)

theorem Finset.Nat.sum_antidiagonal_succ' {N : Type u_2} [AddCommMonoid N] {n : ℕ} {f : ℕ × ℕ → N} : (Finset.sum (Finset.antidiagonal (n + 1)) fun (p : ℕ × ℕ) => f p) = f (n + 1, 0) + Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f (p.1, p.2 + 1)

theorem Finset.Nat.sum_antidiagonal_subst {M : Type u_1} [AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M} : (Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f p n) = Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f p (p.1 + p.2)

theorem Finset.Nat.prod_antidiagonal_subst {M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M} : (Finset.prod (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f p n) = Finset.prod (Finset.antidiagonal n) fun (p : ℕ × ℕ) => f p (p.1 + p.2)

theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk {M : Type u_3} [AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : (Finset.sum (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => f ij) = Finset.sum (Finset.range (Nat.succ n)) fun (k : ℕ) => f (k, n - k)

theorem Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk {M : Type u_3} [CommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : (Finset.prod (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => f ij) = Finset.prod (Finset.range (Nat.succ n)) fun (k : ℕ) => f (k, n - k)

theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ {M : Type u_3} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : (Finset.sum (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => f ij.1 ij.2) = Finset.sum (Finset.range (Nat.succ n)) fun (k : ℕ) => f k (n - k)

This lemma matches more generally than Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk when using rw ← .

theorem Finset.Nat.prod_antidiagonal_eq_prod_range_succ {M : Type u_3} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : (Finset.prod (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => f ij.1 ij.2) = Finset.prod (Finset.range (Nat.succ n)) fun (k : ℕ) => f k (n - k)

This lemma matches more generally than Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk when using rw ← .