Theorem nilpotencyClass_eq_quotient_center_plus_one

Modification history

2026-04-29 17:24

Mathlib/GroupTheory/Nilpotent.lean

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

Deleted nilpotencyClass_eq_quotient_center_plus_one View on Github →

2023-05-31 06:20

Mathlib/GroupTheory/Nilpotent.lean

feat: port GroupTheory.Nilpotent (#4472)

Added nilpotencyClass_eq_quotient_center_plus_one View on Github →