Theorems · Theorem · group theory
Finset.sum_const
∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (b : M), ∑ _x ∈ s, b = s.card • b- Cited by
- 254 results in Mathlib
- Foundations
- Depth 22 from the axioms, rests on 186 definitions · uses propext, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement · cited by 5,195
- Finset.cardstatement and proof · cited by 2,327
- Finset.valproof · cited by 438
- Multiset.sumproof · cited by 388
- Multiset.sum_replicateproof · cited by 30
- Multiset.map_constproof · cited by 9
Cited by254
Results whose statement or proof uses this declaration.
- Finset.card_eq_sum_onesproof · cited by 22
- Finset.card_biUnionproof · cited by 16
- ENNReal.tsum_geometricproof · cited by 8
- Finset.sum_const_natproof · cited by 8
- Finset.expect_constproof · cited by 8
- NumberField.InfinitePlace.sum_mult_eqproof · cited by 7
- Matrix.vecMulVec_eqproof · cited by 7
- Finset.sum_centroidWeights_eq_one_of_card_ne_zeroproof · cited by 6
- Orientation.eq_or_eq_neg_of_isEmptyproof · cited by 6
- groupHomology.comp_d₁₀_eqproof · cited by 6
- MeasureTheory.Measure.count_apply_infiniteproof · cited by 5
- SimpleGraph.Subgraph.IsMatching.even_cardproof · cited by 5
Showing the 200 most cited of 254.