mathlib documentation

algebra.big_operators.nat_antidiagonal

Big operators for nat_antidiagonal #

This file contains theorems relevant to big operators over finset.nat.antidiagonal.

theorem finset.nat.prod_antidiagonal_succ {M : Type u_1} [comm_monoid M] {n : } {f : × → M} :
(finset.nat.antidiagonal (n + 1)).prod (λ (p : × ), f p) = f (0, n + 1) * (finset.nat.antidiagonal n).prod (λ (p : × ), f (p.fst + 1, p.snd))
theorem finset.nat.sum_antidiagonal_succ {N : Type u_2} [add_comm_monoid N] {n : } {f : × → N} :
(finset.nat.antidiagonal (n + 1)).sum (λ (p : × ), f p) = f (0, n + 1) + (finset.nat.antidiagonal n).sum (λ (p : × ), f (p.fst + 1, p.snd))
theorem finset.nat.prod_antidiagonal_swap {M : Type u_1} [comm_monoid M] {n : } {f : × → M} :
(finset.nat.antidiagonal n).prod (λ (p : × ), f p.swap) = (finset.nat.antidiagonal n).prod (λ (p : × ), f p)
theorem finset.nat.sum_antidiagonal_swap {M : Type u_1} [add_comm_monoid M] {n : } {f : × → M} :
(finset.nat.antidiagonal n).sum (λ (p : × ), f p.swap) = (finset.nat.antidiagonal n).sum (λ (p : × ), f p)
theorem finset.nat.prod_antidiagonal_succ' {M : Type u_1} [comm_monoid M] {n : } {f : × → M} :
(finset.nat.antidiagonal (n + 1)).prod (λ (p : × ), f p) = f (n + 1, 0) * (finset.nat.antidiagonal n).prod (λ (p : × ), f (p.fst, p.snd + 1))
theorem finset.nat.sum_antidiagonal_succ' {N : Type u_2} [add_comm_monoid N] {n : } {f : × → N} :
(finset.nat.antidiagonal (n + 1)).sum (λ (p : × ), f p) = f (n + 1, 0) + (finset.nat.antidiagonal n).sum (λ (p : × ), f (p.fst, p.snd + 1))
theorem finset.nat.sum_antidiagonal_subst {M : Type u_1} [add_comm_monoid M] {n : } {f : × → M} :
(finset.nat.antidiagonal n).sum (λ (p : × ), f p n) = (finset.nat.antidiagonal n).sum (λ (p : × ), f p (p.fst + p.snd))
theorem finset.nat.prod_antidiagonal_subst {M : Type u_1} [comm_monoid M] {n : } {f : × → M} :
(finset.nat.antidiagonal n).prod (λ (p : × ), f p n) = (finset.nat.antidiagonal n).prod (λ (p : × ), f p (p.fst + p.snd))
theorem finset.nat.prod_antidiagonal_eq_prod_range_succ_mk {M : Type u_1} [comm_monoid M] (f : × → M) (n : ) :
(finset.nat.antidiagonal n).prod (λ (ij : × ), f ij) = (finset.range n.succ).prod (λ (k : ), 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 : ) :
(finset.nat.antidiagonal n).sum (λ (ij : × ), f ij) = (finset.range n.succ).sum (λ (k : ), f (k, n - k))
theorem finset.nat.sum_antidiagonal_eq_sum_range_succ {M : Type u_1} [add_comm_monoid M] (f : → M) (n : ) :
(finset.nat.antidiagonal n).sum (λ (ij : × ), f ij.fst ij.snd) = (finset.range n.succ).sum (λ (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_1} [comm_monoid M] (f : → M) (n : ) :
(finset.nat.antidiagonal n).prod (λ (ij : × ), f ij.fst ij.snd) = (finset.range n.succ).prod (λ (k : ), f k (n - k))

This lemma matches more generally than finset.nat.prod_antidiagonal_eq_prod_range_succ_mk when using rw ←.