upperCentralSeries_eq_top_iff_nilpotencyClass_le

English

For any n, upperCentralSeries G n = G if and only if nilpotencyClass G ≤ n.

Русский

Для любого n: upperCentralSeries G n = G тогда и только тогда, когда nilpotencyClass G ≤ n.

LaTeX

$$$upperCentralSeries G n = G \iff Group.nilpotencyClass G \\le n$$$

Lean4

theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le {n : ℕ} :
    upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n := by
  classical
  constructor
  · intro h
    exact Nat.find_le h
  · intro h
    rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]
    exact upperCentralSeries_mono _ h

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