least_ascending_central_series_length_eq_nilpotencyClass

English

The nilpotency class equals the smallest n for which the ascending central series reaches G.

Русский

Класс нильпотентности равен наименьшему n, при котором восходящая центральная серия достигает G.

LaTeX

$$$\\min\\{ n \\in \\mathbb{N} \\mid upperCentralSeries(G,n) = G \\} = \\mathrm{Group.nilpotencyClass} G$$$

Lean4

/-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which an ascending
central series reaches `G` in its `n`-th term. -/
theorem least_ascending_central_series_length_eq_nilpotencyClass :
    Nat.find ((nilpotent_iff_finite_ascending_central_series G).mp hG) = Group.nilpotencyClass G :=
  by
  refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
  · intro n hn
    exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
  · rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← top_le_iff, ← hn]
    exact ascending_central_series_le_upper H hH n

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