Theorems · Theorem · group theory

Subgroup.descending_central_series_ge_lower

∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsDescendingCentralSeries H → ∀ (n : ℕ), ⊤.lowerCentralSeries n ≤ H n

Any descending central series for a group is bounded below by the lower central series.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

3 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group