closureCommutatorRepresentatives — Mathlib

English

The subgroup closure of the set of representatives of commutators is the subgroup generated by all commutator representatives.

Русский

Подгруппа closure(commsRepresentatives) образована порожденной всеми представителями коммутаторов.

LaTeX

$$$ \\mathrm{closureCommutatorRepresentatives}(G) = \\operatorname{closure}(\\operatorname{Prod.fst} '' \\operatorname{commutatorRepresentatives}(G) \\cup \\operatorname{Prod.snd} '' \\operatorname{commutatorRepresentatives}(G)) $$$

Lean4

/-- Subgroup generated by representatives `g₁ g₂ : G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/
def closureCommutatorRepresentatives : Subgroup G :=
  closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)

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