Commit 2026-03-03 22:45 98cc46ec

View on Github →

refactor(GroupTheory/Nilpotent): add junk value to Group.nilpotencyClass (#35824) This PR adds a junk value to Group.nilpotencyClass (similar to nilpotencyClass for rings). Can't hurt, since it only makes things more general, and occasionally allows for simpler statements.

Estimated changes

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem Group.nilpotencyClass_def

added theorem Group.nilpotencyClass_of_not_nilpotent

modified theorem nilpotencyClass_quotient_center

modified theorem upperCentralSeries_nilpotencyClass