val_list_prod — Mathlib

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

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