Big operators for nat_antidiagonal #
This file contains theorems relevant to big operators over finset.nat.antidiagonal.
theorem
finset.nat.prod_antidiagonal_swap
{M : Type u_1}
[comm_monoid M]
{n : ℕ}
{f : ℕ × ℕ → M} :
∏ (p : ℕ × ℕ) in finset.nat.antidiagonal n, f p.swap = ∏ (p : ℕ × ℕ) in finset.nat.antidiagonal n, f p
theorem
finset.nat.sum_antidiagonal_swap
{M : Type u_1}
[add_comm_monoid M]
{n : ℕ}
{f : ℕ × ℕ → M} :
∑ (p : ℕ × ℕ) in finset.nat.antidiagonal n, f p.swap = ∑ (p : ℕ × ℕ) in finset.nat.antidiagonal n, f p
theorem
finset.nat.sum_antidiagonal_subst
{M : Type u_1}
[add_comm_monoid M]
{n : ℕ}
{f : ℕ × ℕ → ℕ → M} :
theorem
finset.nat.prod_antidiagonal_subst
{M : Type u_1}
[comm_monoid M]
{n : ℕ}
{f : ℕ × ℕ → ℕ → M} :
theorem
finset.nat.prod_antidiagonal_eq_prod_range_succ_mk
{M : Type u_1}
[comm_monoid M]
(f : ℕ × ℕ → M)
(n : ℕ) :
∏ (ij : ℕ × ℕ) in finset.nat.antidiagonal n, f ij = ∏ (k : ℕ) in finset.range n.succ, f (k, n - k)
theorem
finset.nat.sum_antidiagonal_eq_sum_range_succ_mk
{M : Type u_1}
[add_comm_monoid M]
(f : ℕ × ℕ → M)
(n : ℕ) :
∑ (ij : ℕ × ℕ) in finset.nat.antidiagonal n, f ij = ∑ (k : ℕ) in finset.range n.succ, f (k, n - k)
theorem
finset.nat.sum_antidiagonal_eq_sum_range_succ
{M : Type u_1}
[add_comm_monoid M]
(f : ℕ → ℕ → M)
(n : ℕ) :
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_1}
[comm_monoid M]
(f : ℕ → ℕ → M)
(n : ℕ) :
This lemma matches more generally than finset.nat.prod_antidiagonal_eq_prod_range_succ_mk when
using rw ←.