lowerCentralSeries_eq_bot_iff_nilpotencyClass_le

English

The nth lower central series term is trivial if and only if the nilpotency class is at most n.

Русский

Член γ_n равен ⊥ тогда и только тогда, когда nilpotencyClass G ≤ n.

LaTeX

$$$lowerCentralSeries G n = \\bot \\iff Group.nilpotencyClass G \\le n$$$

Lean4

theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le {n : ℕ} :
    lowerCentralSeries G n = ⊥ ↔ Group.nilpotencyClass G ≤ n := by
  classical
  constructor
  · intro h
    rw [← lowerCentralSeries_length_eq_nilpotencyClass]
    exact Nat.find_le h
  · intro h
    rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]
    exact lowerCentralSeries_antitone h

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