Theorems · Theorem · group theory

List.prod_map_hom

∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (L : List ι) (f : ι → M)
  {G : Type u_8} [inst_2 : FunLike G M N] [MonoidHomClass G M N] (g : G),
  (List.map (⇑g ∘ f) L).prod = g (List.map f L).prod

Defined in

Mathlib.Algebra.BigOperators.Group.List.Basic

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

MonoidMonoidFunLikeMonoidHomClass