English
For a multiset m of M, if every element of m lies in a submonoid S, then m.prod ∈ S.
Русский
Для мультисета элементов M, если каждый элемент принадлежит S, то произведение мультиcета принадлежит S.
LaTeX
$$$m \\text{ is a multiset of } M, \\; \\forall a \\in m, a \\in S \\Rightarrow m.\\operatorname{prod} \\in S$$$
Lean4
/-- Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid. -/
@[to_additive /-- Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is
in the `AddSubmonoid`. -/
]
theorem multiset_prod_mem {M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) :
m.prod ∈ S := by
lift m to Multiset S using hm
rw [← coe_multiset_prod]
exact m.prod.coe_prop
