Theorems · Theorem · combinatorics
Finset.Nat.sum_antidiagonal_eq_sum_range_succ
∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 ij.2 = ∑ k ∈ Finset.range n.succ, f k (n - k)This lemma matches more generally than
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk when using rw ← .
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 71 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 · cited by 1,341
- Finset.HasAntidiagonal.antidiagonalstatement · cited by 218
- Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mkproof · cited by 14
Cited by15
Results whose statement or proof uses this declaration.
- Commute.add_pow'proof · cited by 6
- catalan_succ'proof · cited by 2
- sum_range_powproof · cited by 2
- PowerSeries.coeff_X_mul_largeSchroderSeriesproof · cited by 2
- summable_norm_sum_mul_range_of_summable_normproof · cited by 1
- summable_sum_mul_range_of_summable_norm'proof · cited by 1
- tsum_mul_tsum_eq_tsum_sum_range_of_summable_normproof · cited by 1
- tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'proof · cited by 1
- PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sqproof · cited by 1
- Nat.bell_succ'proof · cited by 0
- PolynomialModule.smul_applyproof · cited by 0
- summable_sum_mul_range_of_summable_mulproof · cited by 0