Theorems · Theorem · ring theory
Finsupp.sum_fintype
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : Fintype α]
(f : α →₀ M) (g : α → M → N), (∀ (i : α), g i 0 = 0) → f.sum g = ∑ i, g i (f i)- Cited by
- 32 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroAddCommMonoidFintype
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.
- DFunLike.coestatement · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- Fintypestatement and proof · cited by 7,736
- Finsuppstatement and proof · cited by 5,255
- Finset.sumstatement · cited by 5,195
- Finset.univstatement and proof · cited by 3,473
- Finsupp.supportproof · cited by 828
- Finsupp.sumstatement · cited by 481
- Finset.subset_univproof · cited by 60
- Finsupp.sum_of_support_subsetproof · cited by 21
Cited by32
Results whose statement or proof uses this declaration.
- Module.Basis.equivFun_symm_applyproof · cited by 22
- Submodule.mem_span_range_iff_exists_funproof · cited by 12
- LinearMap.toMatrix₂_compl₁₂proof · cited by 7
- Module.Basis.constr_apply_fintypeproof · cited by 6
- LinearMap.toMatrix₂'_compl₁₂proof · cited by 6
- Matrix.posSemidef_iff_dotProduct_mulVecproof · cited by 5
- Finsupp.sum_zsmulproof · cited by 4
- PowerBasis.aeval_minpolyGenproof · cited by 3
- Matrix.posDef_iff_dotProduct_mulVecproof · cited by 3
- Convexity.dist_convexCombPair_convexCombPair_leproof · cited by 2
- Finsupp.sum_consproof · cited by 2
- Module.Flat.tfae_equational_criterionproof · cited by 2