nilpotencyClass_zero_iff_subsingleton

English

For a nilpotent group G, NilpotencyClass(G) = 0 if and only if G is subsingleton.

Русский

Для нильпотентной группы G нильпотентность класса 0 эквивалентна тому, что G содержит не более одного элемента.

LaTeX

$$$\\operatorname{nilpotencyClass}(G) = 0 \\;\\Longleftrightarrow\\; G \\text{ is subsingleton}$$$

Lean4

theorem nilpotencyClass_zero_iff_subsingleton [IsNilpotent G] : Group.nilpotencyClass G = 0 ↔ Subsingleton G := by
  classical
    rw [Group.nilpotencyClass, Nat.find_eq_zero, upperCentralSeries_zero, subsingleton_iff_bot_eq_top,
    Subgroup.subsingleton_iff]

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