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} : ∏ p ∈ Finset.antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ Finset.antidiagonal n, f (p.1 + 1, p.2)

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

theorem Finset.Nat.prod_antidiagonal_swap {M : Type u_1} [CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : ∏ p ∈ Finset.antidiagonal n, f p.swap = ∏ p ∈ Finset.antidiagonal n, f p

theorem Finset.Nat.sum_antidiagonal_swap {M : Type u_1} [AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → M} : ∑ p ∈ Finset.antidiagonal n, f p.swap = ∑ p ∈ Finset.antidiagonal n, f p

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

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

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

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

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

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

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

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

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

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