Mathlib Map

Theorems · Theorem · group theory

map_list_sum

∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] {F : Type u_8} [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) (l : List M), f l.sum = (List.map (⇑f) l).sum
Defined in
Mathlib.Algebra.BigOperators.Group.List.Basic
Cited by
31 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext
Assumes
AddMonoidAddMonoidFunLikeAddMonoidHomClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Pi.list_sum_apply · cited by 4Pi.list_sum_applyList.smul_sum · cited by 3List.smul_sumAddSubmonoidClass.coe_list_sum · cited by 2AddSubmonoidClass.coe_lis…Finset.coe_list_sum · cited by 1Finset.coe_list_sumNat.cast_list_sum · cited by 1Nat.cast_list_sumPolynomial.coeff_list_sum · cited by 1Polynomial.coeff_list_sumCharTwo.list_sum_sq · cited by 1CharTwo.list_sum_sqPolynomial.eval₂_list_sum · cited by 1Polynomial.eval₂_list_sumMultiset.map_noncommSum · cited by 1Multiset.map_noncommSumlist_sum_pow_char_pow · cited by 0list_sum_pow_char_powMatrix.conjTranspose_list_sum · cited by 0Matrix.conjTranspose_list…Set.list_sum_singleton · cited by 0Set.list_sum_singletonInt.cast_list_sum · cited by 0Int.cast_list_sumAddSubmonoid.coe_list_sum · cited by 0AddSubmonoid.coe_list_sumList.sum_smul · cited by 0List.sum_smulDFunLike.coe · cited by 62936DFunLike.coeAddMonoid · cited by 2864AddMonoidFunLike · cited by 2560FunLikeAddMonoidHomClass · cited by 252AddMonoidHomClassList.sum_hom · cited by 3List.sum_hommap_list_sumCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by31

Results whose statement or proof uses this declaration.