Commit 2026-05-18 08:56 af782e74

View on Github →

chore(GroupTheory/Nilpotent): to_additivize file (#38753) This PR to_additivizes Nilpotent.lean.

Estimated changes

Modified Mathlib/GroupTheory/Commutator/Finite.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

added def AddSubgroup.lowerCentralSeries

added theorem AddSubgroup.lowerCentralSeries_one

added def AddSubgroup.upperCentralSeriesAux

added theorem AddSubgroup.upperCentralSeries_one

modified theorem Group.isNilpotent_top

modified theorem Subgroup.comap_upperCentralSeries

Modified Mathlib/GroupTheory/Subgroup/Center.lean