Theorem Subgroup.upperCentralSeries.eq_ge_of_eq_gt

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_ge_of_eq_gt View on Github →

2026-04-29 17:24

Mathlib/GroupTheory/Nilpotent.lean

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

Added Subgroup.upperCentralSeries.eq_ge_of_eq_gt View on Github →