commGroup — Mathlib

English

The abelianization G^{ab} carries a natural commutative group structure; in particular, Abelianization G is a commutative group.

Русский

У абеллиановизации G^{ab} естественно задается структура коммутативной группы; в частности, Ab(G) — коммутативная группа.

LaTeX

$$$$ \\mathrm{Abelianization}(G) \\text{ is a } \\mathrm{CommGroup}. $$$$

Lean4

instance commGroup : CommGroup (Abelianization G)
    where
  __ := QuotientGroup.Quotient.group _
  mul_comm x
    y :=
    Quotient.inductionOn₂ x y fun a b ↦
      Quotient.sound' <|
        QuotientGroup.leftRel_apply.mpr <|
          Subgroup.subset_closure
            ⟨b⁻¹, Subgroup.mem_top _, a⁻¹, Subgroup.mem_top _, by simp [commutatorElement_def, mul_assoc]⟩

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