Theorems · Theorem · combinatorics
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk
∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ),
∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij = ∑ k ∈ Finset.range n.succ, f (k, n - k)- Cited by
- 14 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement · cited by 5,195
- Finset.rangestatement and proof · cited by 1,341
- Finset.HasAntidiagonal.antidiagonalstatement · cited by 218
- Finset.sum_mapproof · cited by 115
Cited by14
Results whose statement or proof uses this declaration.
- Finset.Nat.sum_antidiagonal_eq_sum_range_succproof · cited by 15
- Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_evalproof · cited by 3
- Finset.sum_antidiagonal_choose_succ_nsmulproof · cited by 3
- DividedPowers.dpow_add'proof · cited by 3
- bernoulli'_spec'proof · cited by 2
- PowerSeries.exp_mul_exp_eq_exp_addproof · cited by 2
- DividedPowers.dpow_sum'proof · cited by 2
- UpperHalfPlane.qExpansion_mulproof · cited by 1
- Polynomial.gaussNorm_mul_leproof · cited by 1
- Polynomial.coeff_mul_mirrorproof · cited by 1
- DividedPowers.exp_add'proof · cited by 1
- Polynomial.eval_homogenizeproof · cited by 1