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.antidiagonal (n + 1)).prod fun (p : ℕ × ℕ) => f p) = f (0, n + 1) * (Finset.antidiagonal n).prod fun (p : ℕ × ℕ) => f (p.1 + 1, p.2)

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

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

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

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

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

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

theorem Finset.Nat.prod_antidiagonal_subst {M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M} : ((Finset.antidiagonal n).prod fun (p : ℕ × ℕ) => f p n) = (Finset.antidiagonal n).prod 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.antidiagonal n).sum fun (ij : ℕ × ℕ) => f ij) = (Finset.range n.succ).sum 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.antidiagonal n).prod fun (ij : ℕ × ℕ) => f ij) = (Finset.range n.succ).prod 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.antidiagonal n).sum fun (ij : ℕ × ℕ) => f ij.1 ij.2) = (Finset.range n.succ).sum 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.antidiagonal n).prod fun (ij : ℕ × ℕ) => f ij.1 ij.2) = (Finset.range n.succ).prod fun (k : ℕ) => f k (n - k)

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