lowerCentralSeries_nilpotencyClass

English

The bottom term of the lower central series occurs at the nilpotency class: lowerCentralSeries G (nilpotencyClass G) = ⊥.

Русский

Нижняя центральная серия достигает ⊥ на уровне nilpotencyClass G.

LaTeX

$$$lowerCentralSeries G (Group.nilpotencyClass G) = \\bot$$$

Lean4

@[simp]
theorem lowerCentralSeries_nilpotencyClass : lowerCentralSeries G (Group.nilpotencyClass G) = ⊥ := by
  classical
  rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

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