Theorem AddSubgroup.top_lowerCentralSeries_one

Modification history

2026-05-28 22:31

Mathlib/GroupTheory/Nilpotent.lean

fix(GroupTheory/Nilpotent): add back deprecations deleted in #39844 (#39985) …

Deleted AddSubgroup.top_lowerCentralSeries_one View on Github →

2026-05-28 16:48

Mathlib/GroupTheory/Nilpotent.lean

feat(GroupTheory): subgroup-valued lower central series (#39844) …

Added AddSubgroup.top_lowerCentralSeries_one View on Github →