Theorems · Definition · group theory
Subgroup.IsDescendingCentralSeries
{G : Type u_1} → [inst : Group G] → (ℕ → Subgroup G) → PropA sequence of subgroups of G is a descending central series if H 0 is G and
⁅H n, G⁆ ⊆ H (n + 1) for all n. Note that we do not require that H n = {1} for some n.
- Defined in
- Mathlib.GroupTheory.Nilpotent
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- Bracket.bracketproof · cited by 642
Cited by15
Results whose statement or proof uses this declaration.
- Subgroup.lowerCentralSeries_length_eq_nilpotencyClassproof · cited by 5
- Subgroup.nilpotent_iff_finite_descending_central_seriesstatement and proof · cited by 4
- Subgroup.is_ascending_rev_series_of_is_descendingstatement and proof · cited by 3
- Subgroup.is_descending_rev_series_of_is_ascendingstatement · cited by 3
- Subgroup.descending_central_series_ge_lowerstatement and proof · cited by 3
- Subgroup.lowerCentralSeries_isDescendingCentralSeriesstatement · cited by 3
- Subgroup.isNilpotent_iff_lowerCentralSeriesproof · cited by 2
- Subgroup.least_descending_central_series_length_eq_nilpotencyClassstatement and proof · cited by 2
- is_descending_rev_series_of_is_ascendingstatement · cited by 0
- descending_central_series_ge_lowerstatement · cited by 0
- IsDescendingCentralSeriesproof · cited by 0
- lowerCentralSeries_isDescendingCentralSeriesstatement · cited by 0