Theorems · Theorem · combinatorics
Finset.Nat.prod_antidiagonal_succ
∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M},
∏ p ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f p =
f (0, n + 1) * ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f (p.1 + 1, p.2)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetproof · cited by 13,712
- Finset.prodstatement and proof · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
- Finset.prod_mapproof · cited by 75
- Finset.prod_consproof · cited by 60
- Function.Embedding.reflproof · cited by 29
- Function.Embedding.prodMapproof · cited by 23
- Nat.succ_injectiveproof · cited by 14
- Finset.Nat.antidiagonal_succproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Finset.Nat.prod_antidiagonal_succ'proof · cited by 1
- Finset.Nat.sum_antidiagonal_succproof · cited by 1