Def AddSubgroup.lowerCentralSeries

Modification history

2026-05-28 16:48

Mathlib/GroupTheory/Nilpotent.lean

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

Modified AddSubgroup.lowerCentralSeries View on Github →

2026-05-18 08:56

Mathlib/GroupTheory/Nilpotent.lean

chore(GroupTheory/Nilpotent): to_additivize file (#38753) …

Added AddSubgroup.lowerCentralSeries View on Github →