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.Nat.antidiagonal (n + 1)) fun p => f p) = f (0, n + 1) * Finset.prod (Finset.Nat.antidiagonal n) fun p => f (p.fst + 1, p.snd)

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

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

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

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

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

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

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

theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk {M : Type u_3} [AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : (Finset.sum (Finset.Nat.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.Nat.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.Nat.antidiagonal n) fun ij => f ij.fst ij.snd) = 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.Nat.antidiagonal n) fun ij => f ij.fst ij.snd) = 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 ←.