Theorems · Theorem · group theory
Finset.sum_eq_zero
∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M},
(∀ x ∈ s, f x = 0) → ∑ x ∈ s, f x = 0- Cited by
- 139 results in Mathlib
- Foundations
- Depth 56 from the axioms, rests on 874 definitions · 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.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement · cited by 5,195
- Finset.sum_congrproof · cited by 2,323
- Finset.sum_const_zeroproof · cited by 219
Cited by139
Results whose statement or proof uses this declaration.
- Finset.sum_dite_eq'proof · cited by 21
- Finset.sum_dite_eqproof · cited by 12
- Finset.exists_ne_zero_of_sum_ne_zeroproof · cited by 12
- Polynomial.coeff_expandproof · cited by 11
- MonomialOrder.degree_mul_leproof · cited by 10
- Finset.affineCombination_of_eq_one_of_eq_zeroproof · cited by 8
- Finset.sum_subset_zero_on_sdiffproof · cited by 7
- Chebyshev.psi_eq_zero_of_lt_twoproof · cited by 7
- PowerSeries.coeff_X_pow_mul'proof · cited by 7
- Fintype.sum_eq_zeroproof · cited by 7
- MvPowerSeries.le_weightedOrder_mulproof · cited by 7
- MeasureTheory.SimpleFunc.map_setToSimpleFuncproof · cited by 6