noncommProd_mem — Mathlib

English

In a subgroup K of G (with commutativity assumptions on G), a noncommutative product over a finite set with factors in K lies in K.

Русский

Для подгруппы K ⊆ G (при условии коммутативности G) непорядковое произведение элементов из K лежит в K.

LaTeX

$$$(\\forall c \\in t, f c \\in K) \\Rightarrow t.noncommProd f comm \\in K$$$

Lean4

@[to_additive]
theorem noncommProd_mem (K : Subgroup G) {ι : Type*} {t : Finset ι} {f : ι → G} (comm) :
    (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K :=
  K.toSubmonoid.noncommProd_mem t f comm

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