Theorems · Theorem · group theory
Finset.sum_map
∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ) (f : κ → M),
∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x)- Cited by
- 115 results in Mathlib
- Foundations
- Depth 28 from the axioms, rests on 189 definitions · uses propext, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- Multisetproof · cited by 2,627
- Function.Embeddingstatement and proof · cited by 988
- Multiset.mapproof · cited by 876
- Finset.mapstatement and proof · cited by 747
- Finset.valproof · cited by 438
- Multiset.sumproof · cited by 388
- Multiset.map_mapproof · cited by 151
- Finset.map_valproof · cited by 7
Cited by115
Results whose statement or proof uses this declaration.
- PowerSeries.coeff_mulproof · cited by 29
- finsum_eq_sum_of_support_subsetproof · cited by 28
- Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mkproof · cited by 14
- Finset.sum_sigmaproof · cited by 12
- AffineIndependent.comp_embeddingproof · cited by 8
- Finset.sum_disjSumproof · cited by 7
- Affine.Simplex.sum_pointsWithCircumcenterproof · cited by 7
- Nat.sum_divisorsAntidiagonalproof · cited by 6
- Function.Injective.tsum_eqproof · cited by 6
- Finsupp.sum_embDomainproof · cited by 6
- Finset.hasSumproof · cited by 6
- Finset.sum_Ico_add'proof · cited by 6