multiset_noncommProd_mem — Mathlib

English

In a monoid, if S is a submonoid and a multiset m of elements of M has all its elements in S, then the noncommutative product of m with any commuting structure belongs to S.

Русский

В моноиде, если S — подмоноид и мультисет m элементов M имеет все элементы в S, тогда недеприводимый по порядку произведение m с данным commuting-порядком принадлежит S.

LaTeX

$$$$ m.noncommProd comm \in S $$$$

Lean4

@[to_additive]
theorem multiset_noncommProd_mem (S : Submonoid M) (m : Multiset M) (comm) (h : ∀ x ∈ m, x ∈ S) :
    m.noncommProd comm ∈ S :=
  by
  induction m using Quotient.inductionOn with
  | h l => ?_
  simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
  exact Submonoid.list_prod_mem _ h

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