commGroupOfNilpotencyClass — Mathlib

English

Groups with nilpotency class at most 1 are abelian; conversely, abelian groups have nilpotency class at most 1.

Русский

Группы с классом нильпотентности не более 1 абелевы; наоборот, абелевы имеют такой же предел.

LaTeX

$$$\\operatorname{nilpotencyClass}(G) \\le 1 \\iff \\text{Abelian}(G)$$$

Lean4

/-- Groups with nilpotency class at most one are abelian -/
def commGroupOfNilpotencyClass [IsNilpotent G] (h : Group.nilpotencyClass G ≤ 1) : CommGroup G :=
  Group.commGroupOfCenterEqTop <| by
    rw [← upperCentralSeries_one]
    exact upperCentralSeries_eq_top_iff_nilpotencyClass_le.mpr h

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