coe_list_prod — Mathlib

English

In a submonoid of a commutative monoid, the product over a multiset equals the product over its coerced elements.

Русский

Произведение по мультисету в подмономе внутри коммутативного моноида равно произведению образов элементов.

LaTeX

$$$m.\\operatorname{prod} \\in S$$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem coe_list_prod (l : List S) : (l.prod : M) = (l.map (↑)).prod :=
  map_list_prod (SubmonoidClass.subtype S : _ →* M) l

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