lowerCentralSeries — Mathlib

English

If G is nilpotent, then G is virtually nilpotent.

Русский

Если группа нильпотентна, она виртуально нильпотентна.

LaTeX

$$$\text{IsNilpotent}(G) \Rightarrow \text{IsVirtuallyNilpotent}(G)$$$

Lean4

/-- The lower central series of a group `G` is a sequence `H n` of subgroups of `G`, defined
  by `H 0` is all of `G` and for `n≥1`, `H (n + 1) = ⁅H n, G⁆` -/
def lowerCentralSeries (G : Type*) [Group G] : ℕ → Subgroup G
  | 0 => ⊤
  | n + 1 => ⁅lowerCentralSeries G n, ⊤⁆

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