isCyclic_abelianization — Mathlib

English

Let G be a finite Z-group. Then the abelianization of G, i.e., G modulo its commutator subgroup, is cyclic.

Русский

Пусть G — конечная Z-группа. Тогда абеллизация G, то есть G/([G,G]), циклична.

LaTeX

$$$IsCyclic(\\mathrm{Abelianization}(G))$$$

Lean4

/-- A finite Z-group has cyclic abelianization. -/
instance isCyclic_abelianization [Finite G] [IsZGroup G] : IsCyclic (Abelianization G) :=
  let _ : IsZGroup (Abelianization G) := inferInstanceAs (IsZGroup (G ⧸ commutator G))
  inferInstance

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