mathlib3 documentation

algebra.big_operators.nat_antidiagonal

Big operators for `nat_antidiagonal` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ←.