nilpotent_iff_finite_ascending_central_series

English

A group G is nilpotent if and only if there exists n with upperCentralSeries G n = ⊤.

Русский

Группа G нильпотентна тогда и только тогда, когда существует n, для которого upperCentralSeries G n = ⊤.

LaTeX

$$$\exists n:\mathbb{N},\ upperCentralSeries(G,n)=\top$$$

Lean4

/-- A group `G` is nilpotent iff there exists an ascending central series which reaches `G` in
  finitely many steps. -/
theorem nilpotent_iff_finite_ascending_central_series :
    IsNilpotent G ↔ ∃ n : ℕ, ∃ H : ℕ → Subgroup G, IsAscendingCentralSeries H ∧ H n = ⊤ :=
  by
  constructor
  · rintro ⟨n, nH⟩
    exact ⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩
  · rintro ⟨n, H, hH, hn⟩
    use n
    rw [eq_top_iff, ← hn]
    exact ascending_central_series_le_upper H hH n

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