multiset_prod_mem — Mathlib

English

Let M be a commutative monoid and S a submonoid. For any multiset m of M, if every element of m lies in S, then the product of m lies in S.

Русский

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

LaTeX

$$$$ m.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] (S : Submonoid M) (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S :=
  _root_.multiset_prod_mem m hm

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