Commit 2026-10-20 17:59 b90676dd

View on Github →

chore(GroupTheory/Nilpotent): split off material on lower central series (#43348) GroupTheory/Nilpotent.lean is getting rather long and messy. This PR splits off the material on lower central series to a new file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

deleted def AddSubgroup.lowerCentralSeries

deleted def Subgroup.IsDescendingCentralSeries

deleted theorem Subgroup.derived_le_lower_central

deleted theorem Subgroup.descending_central_series_ge_lower

deleted theorem Subgroup.lowerCentralSeries.map

deleted def Subgroup.lowerCentralSeries

deleted theorem Subgroup.lowerCentralSeries_antitone

deleted theorem Subgroup.lowerCentralSeries_isDescendingCentralSeries

deleted theorem Subgroup.lowerCentralSeries_le_self

deleted theorem Subgroup.lowerCentralSeries_map_subtype_le

deleted theorem Subgroup.lowerCentralSeries_mono

deleted theorem Subgroup.lowerCentralSeries_one_eq_bot_iff

deleted theorem Subgroup.lowerCentralSeries_pi_le

deleted theorem Subgroup.lowerCentralSeries_pi_of_finite

deleted theorem Subgroup.lowerCentralSeries_prod

deleted theorem Subgroup.lowerCentralSeries_succ

deleted theorem Subgroup.lowerCentralSeries_succ_eq_bot

deleted theorem Subgroup.lowerCentralSeries_zero

deleted theorem Subgroup.map_lowerCentralSeries

deleted theorem Subgroup.mem_lowerCentralSeries_succ_iff

deleted theorem Subgroup.self_le_normalizer_lowerCentralSeries

deleted theorem Subgroup.top_lowerCentralSeries_one

deleted theorem Subgroup.top_lowerCentralSeries_pi_le

deleted theorem Subgroup.top_lowerCentralSeries_pi_of_finite

deleted theorem Subgroup.top_lowerCentralSeries_prod

deleted theorem Subgroup.top_subtype_lowerCentralSeries

Created Mathlib/GroupTheory/Nilpotent/LowerCentralSeries.lean

added def AddSubgroup.lowerCentralSeries

added def Subgroup.IsDescendingCentralSeries

added theorem Subgroup.derivedSeries_le_lowerCentralSeries_top

added theorem Subgroup.descending_central_series_ge_lower

added theorem Subgroup.lowerCentralSeries.map

added def Subgroup.lowerCentralSeries

added theorem Subgroup.lowerCentralSeries_antitone

added theorem Subgroup.lowerCentralSeries_isDescendingCentralSeries

added theorem Subgroup.lowerCentralSeries_le_self

added theorem Subgroup.lowerCentralSeries_map_subtype_le

added theorem Subgroup.lowerCentralSeries_mono

added theorem Subgroup.lowerCentralSeries_one_eq_bot_iff

added theorem Subgroup.lowerCentralSeries_pi_le

added theorem Subgroup.lowerCentralSeries_pi_of_finite

added theorem Subgroup.lowerCentralSeries_prod

added theorem Subgroup.lowerCentralSeries_succ

added theorem Subgroup.lowerCentralSeries_succ_eq_bot

added theorem Subgroup.lowerCentralSeries_zero

added theorem Subgroup.map_lowerCentralSeries

added theorem Subgroup.mem_lowerCentralSeries_succ_iff

added theorem Subgroup.self_le_normalizer_lowerCentralSeries

added theorem Subgroup.top_lowerCentralSeries_one

added theorem Subgroup.top_lowerCentralSeries_pi_le

added theorem Subgroup.top_lowerCentralSeries_pi_of_finite

added theorem Subgroup.top_lowerCentralSeries_prod

added theorem Subgroup.top_subtype_lowerCentralSeries