Documentation

Mathlib.Algebra.BigOperators.NatAntidiagonal

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} [inst : ] {n : } {f : M} :
(Finset.prod (Finset.Nat.antidiagonal (n + 1)) fun p => f p) = f (0, n + 1) * Finset.prod () fun p => f (p.fst + 1, p.snd)
theorem Finset.Nat.sum_antidiagonal_succ {N : Type u_1} [inst : ] {n : } {f : N} :
(Finset.sum (Finset.Nat.antidiagonal (n + 1)) fun p => f p) = f (0, n + 1) + Finset.sum () fun p => f (p.fst + 1, p.snd)
theorem Finset.Nat.sum_antidiagonal_swap {M : Type u_1} [inst : ] {n : } {f : M} :
(Finset.sum () fun p => f ()) = Finset.sum () fun p => f p
theorem Finset.Nat.prod_antidiagonal_swap {M : Type u_1} [inst : ] {n : } {f : M} :
(Finset.prod () fun p => f ()) = Finset.prod () fun p => f p
theorem Finset.Nat.prod_antidiagonal_succ' {M : Type u_1} [inst : ] {n : } {f : M} :
(Finset.prod (Finset.Nat.antidiagonal (n + 1)) fun p => f p) = f (n + 1, 0) * Finset.prod () fun p => f (p.fst, p.snd + 1)
theorem Finset.Nat.sum_antidiagonal_succ' {N : Type u_1} [inst : ] {n : } {f : N} :
(Finset.sum (Finset.Nat.antidiagonal (n + 1)) fun p => f p) = f (n + 1, 0) + Finset.sum () fun p => f (p.fst, p.snd + 1)
theorem Finset.Nat.sum_antidiagonal_subst {M : Type u_1} [inst : ] {n : } {f : M} :
(Finset.sum () fun p => f p n) = Finset.sum () fun p => f p (p.fst + p.snd)
theorem Finset.Nat.prod_antidiagonal_subst {M : Type u_1} [inst : ] {n : } {f : M} :
(Finset.prod () fun p => f p n) = Finset.prod () fun p => f p (p.fst + p.snd)
theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk {M : Type u_1} [inst : ] (f : M) (n : ) :
(Finset.sum () fun ij => f ij) = Finset.sum () fun k => f (k, n - k)
theorem Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk {M : Type u_1} [inst : ] (f : M) (n : ) :
(Finset.prod () fun ij => f ij) = Finset.prod () fun k => f (k, n - k)
theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ {M : Type u_1} [inst : ] (f : M) (n : ) :
(Finset.sum () fun ij => f ij.fst ij.snd) = Finset.sum () 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_1} [inst : ] (f : M) (n : ) :
(Finset.prod () fun ij => f ij.fst ij.snd) = Finset.prod () fun k => f k (n - k)

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