Theorem AddSubgroup.lowerCentralSeries_one

Modification history

2026-05-28 16:48

Mathlib/GroupTheory/Nilpotent.lean

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

Deleted AddSubgroup.lowerCentralSeries_one View on Github →

2026-05-18 08:56

Mathlib/GroupTheory/Nilpotent.lean

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

Added AddSubgroup.lowerCentralSeries_one View on Github →