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} :

theorem finset.nat.sum_antidiagonal_succ {N : Type u_2} [add_comm_monoid N] {n : ℕ} {f : ℕ × ℕ → N} :

theorem finset.nat.prod_antidiagonal_swap {M : Type u_1} [comm_monoid M] {n : ℕ} {f : ℕ × ℕ → M} :

theorem finset.nat.sum_antidiagonal_swap {M : Type u_1} [add_comm_monoid M] {n : ℕ} {f : ℕ × ℕ → M} :

theorem finset.nat.prod_antidiagonal_succ' {M : Type u_1} [comm_monoid M] {n : ℕ} {f : ℕ × ℕ → M} :

theorem finset.nat.sum_antidiagonal_succ' {N : Type u_2} [add_comm_monoid N] {n : ℕ} {f : ℕ × ℕ → N} :

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 : ℕ) :

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 : ℕ) :

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

Big operators for nat_antidiagonal #