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} :
∏ (p : × ) in finset.nat.antidiagonal (n + 1), f p = (f (0, n + 1)) * ∏ (p : × ) in finset.nat.antidiagonal n, f (p.fst + 1, p.snd)
theorem finset.nat.sum_antidiagonal_succ {N : Type u_2} [add_comm_monoid N] {n : } {f : × → N} :
∑ (p : × ) in finset.nat.antidiagonal (n + 1), f p = f (0, n + 1) + ∑ (p : × ) in finset.nat.antidiagonal n, f (p.fst + 1, p.snd)
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.prod_antidiagonal_succ' {M : Type u_1} [comm_monoid M] {n : } {f : × → M} :
∏ (p : × ) in finset.nat.antidiagonal (n + 1), f p = (f (n + 1, 0)) * ∏ (p : × ) in finset.nat.antidiagonal n, f (p.fst, p.snd + 1)
theorem finset.nat.sum_antidiagonal_succ' {N : Type u_2} [add_comm_monoid N] {n : } {f : × → N} :
∑ (p : × ) in finset.nat.antidiagonal (n + 1), f p = f (n + 1, 0) + ∑ (p : × ) in finset.nat.antidiagonal n, f (p.fst, p.snd + 1)
theorem finset.nat.sum_antidiagonal_subst {M : Type u_1} [add_comm_monoid M] {n : } {f : × → M} :
∑ (p : × ) in finset.nat.antidiagonal n, f p n = ∑ (p : × ) in finset.nat.antidiagonal n, f p (p.fst + p.snd)
theorem finset.nat.prod_antidiagonal_subst {M : Type u_1} [comm_monoid M] {n : } {f : × → M} :
∏ (p : × ) in finset.nat.antidiagonal n, f p n = ∏ (p : × ) in finset.nat.antidiagonal n, 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 : ) :
∏ (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 : ) :
∑ (ij : × ) in finset.nat.antidiagonal n, f ij.fst ij.snd = ∑ (k : ) in finset.range n.succ, f k (n - k)
theorem finset.nat.prod_antidiagonal_eq_prod_range_succ {M : Type u_1} [comm_monoid M] (f : → M) (n : ) :
∏ (ij : × ) in finset.nat.antidiagonal n, f ij.fst ij.snd = ∏ (k : ) in 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 ←.