prod_hom — Mathlib

English

For any multiset s in M and any MonoidHom f, the product of the mapped elements equals the map of the product: (map f s).prod = f(s.prod).

Русский

Для любого мультимножества s в моноиде M и гомоморфизма f выполняется: prod(map f s) = f(prod s).

LaTeX

$$$ (s.map f).prod = f\, s.prod $$$

Lean4

@[to_additive]
theorem prod_hom (s : Multiset M) {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) :
    (s.map f).prod = f s.prod :=
  Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

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