commutator — Mathlib

English

The commutator subgroup of G is the normal subgroup generated by all commutators [p,q] = p q p^{-1} q^{-1}.

Русский

Коммутаторная подгруппа группы G есть нормальная подгруппа, генерируемая всеми коммутаторами [p,q] = p q p^{-1} q^{-1}.

LaTeX

$$$\\text{commutator}(G) = [\\top,\\top]$$$

Lean4

/-- The commutator subgroup of a group G is the normal subgroup
  generated by the commutators [p,q]=`p*q*p⁻¹*q⁻¹`. -/
def commutator : Subgroup G :=
  ⁅(⊤ : Subgroup G), ⊤⁆
deriving Subgroup.Normal, Subgroup.Characteristic

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