coe_multiset_prod — Mathlib

English

Let M be a commutative monoid and S a submonoid of M. For any multiset m of elements of S, the product of the elements of m computed in M equals the product of the same elements viewed in M via the inclusion S → M.

Русский

Пусть M — коммутативный моноид, S — подмономод M. Для любой мультисет m элементов из S произведение элементов m в M равно произведению тех же элементов, рассматриваемых как элементы M через включение S → M.

LaTeX

$$$$ (m.prod : M) = (m.map (\\uparrow)).prod $$$$

Lean4

@[to_additive (attr := norm_cast)]
theorem coe_multiset_prod {M} [CommMonoid M] (S : Submonoid M) (m : Multiset S) : (m.prod : M) = (m.map (↑)).prod :=
  S.subtype.map_multiset_prod m

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