Commit 2026-03-17 11:27 ea243b7d

View on Github →

feat(GroupTheory/Nilpotent): remove [IsNilpotent] assumption from some theorems (#36093) This PR uses the junk value of nilpotencyClass to remove [IsNilpotent] assumption from some theorems.

Estimated changes

Modified Mathlib/GroupTheory/Nilpotent.lean

modified theorem nilpotencyClass_le_of_upperCentralSeries_eq

modified theorem upperCentralSeries.StrictMonoOn

modified theorem upperCentralSeries.card_image_eq_of_le_nilpotencyClass