Theorems · Theorem · combinatorics
Fintype.sum_eq_single
∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] {f : α → M} (a : α),
(∀ (x : α), x ≠ a → f x = 0) → ∑ x, f x = f a- Defined in
- Mathlib.Data.Fintype.BigOperators
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeAddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Fintypestatement and proof · cited by 7,736
- Finset.sumstatement · cited by 5,195
- Finset.univstatement and proof · cited by 3,473
- Finset.mem_univproof · cited by 361
- Finset.sum_eq_singleproof · cited by 98
Cited by16
Results whose statement or proof uses this declaration.
- PiLp.nnnorm_singleproof · cited by 4
- InnerProductSpace.canonicalCovariantTensor_eq_sumproof · cited by 3
- Matrix.adjugate_fin_succ_eq_det_submatrixproof · cited by 2
- Ideal.quotientInfToPiQuotient_surjproof · cited by 2
- Matrix.IsTotallyUnimodular.fromRows_unitlikeproof · cited by 1
- AlgHom.eq_piEvalAlgHomproof · cited by 1
- Matrix.rank_le_card_of_support_subsetproof · cited by 1
- QuadraticMap.pi_apply_singleproof · cited by 0
- Matrix.blockDiagonal'_mulproof · cited by 0
- PowerBasis.leftMulMatrixproof · cited by 0