Theorems · Theorem · ring theory
Finsupp.finsetSum_apply
∀ {α : Type u_1} {ι : Type u_2} {N : Type u_10} [inst : AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α),
(∑ i ∈ S, f i) a = ∑ i ∈ S, (f i) a- Cited by
- 6 results in Mathlib
- Foundations
- Depth 70 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement and proof · cited by 5,255
- Finset.sumstatement · cited by 5,195
- map_sumproof · cited by 455
- Finsupp.applyAddHomproof · cited by 3
Cited by6
Results whose statement or proof uses this declaration.
- Finsupp.sum_applyproof · cited by 27
- TensorProduct.vanishesTrivially_of_sum_tmul_eq_zeroproof · cited by 2
- Module.Flat.tfae_equational_criterionproof · cited by 2
- KaehlerDifferential.range_kerCotangentToTensorproof · cited by 1
- Nat.factorization_prod_applyproof · cited by 1
- Finsupp.finset_sum_applyproof · cited by 0