lowerCentralSeries_length_eq_nilpotencyClass

English

The nilpotency class equals the length of the lower central series.

Русский

Класс нильпотентности равен длине нижней центральной серии.

LaTeX

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

Lean4

/-- The nilpotency class of a nilpotent `G` is equal to the length of the lower central series. -/
theorem lowerCentralSeries_length_eq_nilpotencyClass :
    Nat.find (nilpotent_iff_lowerCentralSeries.mp hG) = Group.nilpotencyClass (G := G) :=
  by
  rw [← least_descending_central_series_length_eq_nilpotencyClass]
  refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
  · rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← le_bot_iff, ← hn]
    exact descending_central_series_ge_lower H hH n
  · rintro n h
    exact ⟨lowerCentralSeries G, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩

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