commGroup — Mathlib

English

For any group G, the quotient by its commutator subgroup G/[G,G] is an abelian group.

Русский

Для любой группы G смещение по коммутаторной подгруппе G/[G,G] даёт абелеву группу.

LaTeX

$$$G/[G,G] \\in \\mathbf{Ab}$$$

Lean4

instance commGroup : CommGroup (G_ab G)
    where
  mul_comm := fun x y =>
    Quotient.inductionOn₂' x y fun a b =>
      Quotient.sound' <|
        QuotientGroup.leftRel_apply.mpr <|
          by
          have h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆ := by group
          rw [h]
          exact
            Subgroup.le_topologicalClosure _
              (Subgroup.commutator_mem_commutator (Subgroup.mem_top b⁻¹) (Subgroup.mem_top a⁻¹))
  __ : Group (G_ab G) := inferInstance

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