upperCentralSeries_nilpotencyClass

English

For a nilpotent group G, the nth upper central series reaches G at n = nilpotencyClass G.

Русский

Для нильпотентной группы G верхняя центральная серия достигает всей группы на уровне n = nilpotencyClass G.

LaTeX

$$$\\operatorname{upperCentralSeries}(G, \\mathrm{Group.nilpotencyClass} G) = G$$$

Lean4

@[simp]
theorem upperCentralSeries_nilpotencyClass : upperCentralSeries G (Group.nilpotencyClass G) = ⊤ :=
  Nat.find_spec (IsNilpotent.nilpotent G)

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