Theorems · Theorem · group theory
Finset.sum_const_zero
∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M], ∑ _x ∈ s, 0 = 0- Cited by
- 219 results in Mathlib
- Foundations
- Depth 23 from the axioms, rests on 187 definitions · uses propext, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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.valproof · cited by 438
- Multiset.sumproof · cited by 388
- Multiset.cardproof · cited by 375
- nsmul_zeroproof · cited by 73
- Multiset.map_const'proof · cited by 39
- Multiset.sum_replicateproof · cited by 30
Cited by219
Results whose statement or proof uses this declaration.
- Finset.sum_eq_zeroproof · cited by 139
- Finset.sum_eq_singleproof · cited by 98
- Finset.sum_nonnegproof · cited by 91
- Finsupp.sum_fun_zeroproof · cited by 29
- linearIndependent_iff'proof · cited by 22
- Finset.sum_posproof · cited by 15
- hasSum_zeroproof · cited by 13
- affineCombination_mem_affineSpanproof · cited by 12
- dotProduct_zeroproof · cited by 11
- Finset.sum_disjiUnionproof · cited by 10
- zero_dotProductproof · cited by 9
- Finset.sum_pos'proof · cited by 9
Showing the 200 most cited of 219.