Theorems · Theorem · group theory
finsum_eq_single
∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] (f : α → M) (a : α),
(∀ (x : α), x ≠ a → f x = 0) → ∑ᶠ (x : α), f x = f a- Defined in
- Mathlib.Algebra.BigOperators.Finprod
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- SetLike.coeproof · cited by 8,199
- Function.supportproof · cited by 610
- finsumstatement · cited by 286
- Finset.sum_singletonproof · cited by 251
- Set.mem_singleton_iffproof · cited by 172
- Finset.coe_singletonproof · cited by 145
- Function.mem_supportproof · cited by 54
- finsum_eq_sum_plift_of_support_subsetproof · cited by 5
- PLift.eq_up_iff_down_eqproof · cited by 1
Cited by18
Results whose statement or proof uses this declaration.
- MvPowerSeries.coeff_expand_smulproof · cited by 7
- finsum_uniqueproof · cited by 3
- HahnSeries.SummableFamily.hsum_orderTop_of_leproof · cited by 2
- MvPowerSeries.subst_zero_eq_C_constantCoeffproof · cited by 2
- PowerSeries.coeff_subst_X_powproof · cited by 2
- HahnSeries.SummableFamily.hsum_leadingCoeff_of_leproof · cited by 1
- MvPowerSeries.map_algebraMap_eq_subst_Xproof · cited by 1
- HahnSeries.SummableFamily.hsum_singleproof · cited by 1
- FormalGroup.coeff_one_Xzeroproof · cited by 1
- FormalGroup.coeff_one_zeroXproof · cited by 1
- HahnSeries.SummableFamily.powerSeriesFamily_hsum_zeroproof · cited by 1
- PowerSeries.coeff_subst_singleproof · cited by 1