Theorem Subgroup.upperCentralSeries.eq_ge_of_eq_succ

Modification history

2026-04-29 17:24

Mathlib/GroupTheory/Nilpotent.lean

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

Added Subgroup.upperCentralSeries.eq_ge_of_eq_succ View on Github →