Theorems · Theorem · group theory
Finset.sum_eq_single
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι),
(∀ b ∈ s, b ≠ a → f b = 0) → (a ∉ s → f a = 0) → ∑ x ∈ s, f x = f a- Cited by
- 98 results in Mathlib
- Foundations
- Depth 69 from the axioms, rests on 1,331 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Finset.sum_eq_single_of_memproof · cited by 33
- by_casesproof · cited by 31
Cited by98
Results whose statement or proof uses this declaration.
- Matrix.det_diagonalproof · cited by 27
- Finset.sum_dite_eq'proof · cited by 21
- Polynomial.coeff_zero_eq_eval_zeroproof · cited by 20
- Finsupp.sum_eq_singleproof · cited by 18
- Fintype.sum_eq_singleproof · cited by 16
- Polynomial.coeff_derivativeproof · cited by 14
- Finset.sum_dite_eqproof · cited by 12
- Polynomial.coeff_expandproof · cited by 11
- single_dotProductproof · cited by 10
- Matrix.toLin_selfproof · cited by 9
- linearIndependent_iff'ₛproof · cited by 9
- Polynomial.coeff_mul_X_powproof · cited by 9