English
Let G be a commutative group and H a subgroup of G. If m is a multiset consisting of elements of H, then the product of all elements of m, viewed in G, is equal to the product of the corresponding elements in G obtained by forgetting their subgroup membership (i.e., via the inclusion map H → G).
Русский
Пусть G—коммутативная группа, H— подгруппа G. Пусть m — мультинабор элементов из H. Произведение элементов m в G равно произведению соответствующих элементов в G, полученных проходом через включение H в G.
LaTeX
$$$(m.prod : G) = (m.map \operatorname{Subtype.val}).prod$$$
Lean4
@[to_additive (attr := simp 1100, norm_cast)]
theorem val_multiset_prod {G} [CommGroup G] (H : Subgroup G) (m : Multiset H) :
(m.prod : G) = (m.map Subtype.val).prod :=
SubmonoidClass.coe_multiset_prod m
