English
Let S be a submonoid of M. For a multiset m and a commuting pattern comm, if every element of m lies in S, then the noncommutative product m.noncommProd comm lies in S.
Русский
Пусть S — подмономод M. Для мультиcета m и соответствующего шаблона коммутирования comm, если каждый элемент m принадлежит S, то произведение m.noncommProd comm принадлежит S.
LaTeX
$$$$ m.noncommProd comm \\in S $$$$
Lean4
@[to_additive (attr := aesop 90% (rule_sets := [SetLike]))]
theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M} (hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S
| 0 => by
rw [pow_zero]
exact OneMemClass.one_mem S
| n + 1 => by
rw [pow_succ]
exact mul_mem (pow_mem hx n) hx
