nilpotencyClass_le_one — Mathlib

English

If a group has nilpotency class at most one, then it is abelian.

Русский

Если класс нильпотентности группы не превосходит единицы, то она абелева.

LaTeX

$$$\\operatorname{nilpotencyClass}(G) \\le 1 \\Rightarrow G \\text{ is abelian}$$$

Lean4

/-- Abelian groups have nilpotency class at most one -/
theorem nilpotencyClass_le_one {G : Type*} [CommGroup G] : Group.nilpotencyClass G ≤ 1 :=
  by
  rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]
  apply CommGroup.center_eq_top

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