Theorem Subgroup.lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_top

Modification history

2026-06-02 11:20
Mathlib/GroupTheory/Nilpotent.lean
feat(GroupTheory/Nilpotent): a nontrivial nilpotent group has a nontrivial center (#39950) …
Added Subgroup.lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_topView on Github →