Theorem Group.nilpotencyClass_eq_quotient_center_add_one

Modification history

2026-10-06 22:43
Mathlib/GroupTheory/Nilpotent.lean
chore: deprecate `plus` and `minus` in names (#44566) …
Added Group.nilpotencyClass_eq_quotient_center_add_oneView on Github →