English
The product of a list of elements from a subgroup, when embedded in G, equals the product of their images in G after taking their values.
Русский
Произведение списка элементов из подгруппы, отображенное в G, равно произведению их значений в G.
LaTeX
$$$\\mathrm{val}(\\mathrm{l}.prod) = (\\mathrm{List}.map \\mathrm{Subtype}.val \\mathrm{l}).prod$$$
Lean4
@[to_additive (attr := simp 1100, norm_cast)]
theorem val_list_prod (l : List H) : (l.prod : G) = (l.map Subtype.val).prod :=
SubmonoidClass.coe_list_prod l