map_list_prod — Mathlib

English

For monoids, applying a monoid hom to the product over a list equals the product of the hom applied to each element.

Русский

Для моноидов отображение моноидной гомоморфной функции применяется к произведению списка и даёт произведение значений гомоморфа по элементам списка.

LaTeX

$$$f l.prod = (l.map f).prod$$

Lean4

@[to_additive]
theorem map_list_prod {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) (l : List M) :
    f l.prod = (l.map f).prod :=
  (l.prod_hom f).symm

Похожие утверждения