Theorems · Theorem · group theory
Finset.sum_singleton
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (f : ι → M) (a : ι), ∑ x ∈ {a}, f x = f a- Cited by
- 251 results in Mathlib
- Foundations
- Depth 26 from the axioms, rests on 173 definitions · uses propext, 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.
- Finsetstatement · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement · cited by 5,195
- add_zeroproof · cited by 2,707
- Finset.fold_singletonproof · cited by 2
Cited by251
Results whose statement or proof uses this declaration.
- Finsupp.sum_single_indexproof · cited by 130
- Fin.sum_univ_twoproof · cited by 49
- MeasureTheory.measure_union_leproof · cited by 43
- Complex.exp_zeroproof · cited by 43
- Polynomial.mul_coeff_zeroproof · cited by 37
- Finset.single_le_sumproof · cited by 34
- Matrix.det_fin_twoproof · cited by 33
- Finset.sum_eq_single_of_memproof · cited by 33
- tsum_eq_singleproof · cited by 19
- finsum_eq_singleproof · cited by 18
- Summable.tendsto_cofinite_zeroproof · cited by 16
- MeasureTheory.VectorMeasure.enorm_measure_le_variationproof · cited by 15
Showing the 200 most cited of 251.