Theorem Subgroup.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) …

Modified Subgroup.upperCentralSeries.eq_top View on Github →

2026-04-29 17:24

Mathlib/GroupTheory/Nilpotent.lean

chore(GroupTheory/Nilpotent): move declarations into namespace (#37175) …

Added Subgroup.upperCentralSeries.eq_top View on Github →