Theorems · Theorem · linear algebra
Finsupp.smul_sum
∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_5} [inst : Zero β] [inst_1 : AddCommMonoid M]
[inst_2 : DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M}, c • v.sum h = v.sum fun a b => c • h a b- Defined in
- Mathlib.LinearAlgebra.Finsupp.LSum
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroAddCommMonoidDistribSMul
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.
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement and proof · cited by 5,255
- Finsupp.sumstatement · cited by 481
- DistribSMulstatement and proof · cited by 117
- Finset.smul_sumproof · cited by 88
Cited by11
Results whose statement or proof uses this declaration.
- MvPolynomial.pderiv_monomialproof · cited by 4
- Submodule.mem_ideal_smul_span_iff_exists_sumproof · cited by 3
- Finsupp.linearCombination_linearCombinationproof · cited by 2
- Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoinproof · cited by 2
- Convexity.iConvexComb_commproof · cited by 1
- Finsupp.sum_smul_index_semilinearMap'proof · cited by 1
- Polynomial.smul_sumproof · cited by 1
- LinearMap.commute_transvections_iff_of_basisproof · cited by 0
- groupHomology.isBoundary₀_of_mem_coinvariantsKerproof · cited by 0
- SkewMonoidAlgebra.smul_sumproof · cited by 0
- SkewPolynomial.smul_sumproof · cited by 0