Theorems · Theorem · group theory

List.prod_hom

∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (l : List M) {F : Type u_8}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N] (f : F), (List.map (⇑f) l).prod = f l.prod

Defined in

Mathlib.Algebra.BigOperators.Group.List.Basic

Cited by

8 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

MonoidMonoidFunLikeMonoidHomClass