Theorems · Definition · group theory
Subgroup.lowerCentralSeries
{G : Type u_1} → [inst : Group G] → Subgroup G → ℕ → Subgroup GThe lower central series of a subgroup S of G, computed in the ambient group G.
This is the iterated commutator ⁅⁅⋯⁅S, S⁆, S⁆⋯, S⁆, a subgroup of G. The lower central series
of G itself is the case S = ⊤.
- Defined in
- Mathlib.GroupTheory.Nilpotent
- Cited by
- 57 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by58
Results whose statement or proof uses this declaration.
- Subgroup.nilpotent_iff_lowerCentralSeriesstatement · cited by 9
- Subgroup.lowerCentralSeries_length_eq_nilpotencyClassstatement and proof · cited by 5
- Subgroup.lowerCentralSeries_monostatement and proof · cited by 5
- Subgroup.lowerCentralSeries_succstatement · cited by 5
- Subgroup.top_subtype_lowerCentralSeriesstatement and proof · cited by 4
- Subgroup.map_lowerCentralSeriesstatement and proof · cited by 4
- Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_lestatement and proof · cited by 4
- Subgroup.descending_central_series_ge_lowerstatement · cited by 3
- Subgroup.lowerCentralSeries_isDescendingCentralSeriesstatement and proof · cited by 3
- Subgroup.lowerCentralSeries_succ_eq_botstatement and proof · cited by 3
- Subgroup.lowerCentralSeries_antitonestatement and proof · cited by 3
- Subgroup.lowerCentralSeries_nilpotencyClassstatement and proof · cited by 3