coe_list_prod — Mathlib

English

For a Submonoid S of M and a list l of elements of S, the product in M of l equals the product of the coerced list elements.

Русский

Для подмонома S и списка l элементов S произведение в M равняется произведению образов элементов l.

LaTeX

$$$\\text{l.prod} = (\\text{l.map}(\\uparrow)).prod$ in M$$

Lean4

@[to_additive (attr := norm_cast)]
theorem coe_list_prod (l : List s) : (l.prod : M) = (l.map (↑)).prod :=
  map_list_prod s.subtype l

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