multiset_noncommProd_mem — Mathlib

English

If a multiset g has pairwise commuting elements and all its elements lie in K, then the noncommutative product g.noncommProd lies in K.

Русский

Если элементы мультисеета пары коммутируют друг с другом и все элементы принадлежат K, то произведение без учёта порядка лежит в K.

LaTeX

$$$(\\forall a \\in g, a \\in K) \\land (\\text{Pairwise Commute } g) \\Rightarrow g.noncommProd \\in K$$$

Lean4

@[to_additive]
theorem multiset_noncommProd_mem (K : Subgroup G) (g : Multiset G) (comm) : (∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K :=
  K.toSubmonoid.multiset_noncommProd_mem g comm

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