Commit 2026-02-26 23:01 917a081c

View on Github →

feat: a nilpotent simple group is cyclic (#34318) This PR also adds some API around nilpotencyClass and upperCentralSeries.

Estimated changes

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem nilpotencyClass_le_of_upperCentralSeries_eq

added theorem nilpotencyClass_le_one_of_isSimple_of_isNilpotent

added theorem upperCentralSeries.StrictMonoOn

added theorem upperCentralSeries.card_image_eq_of_le_nilpotencyClass

added theorem upperCentralSeries.eq_ge_of_eq_gt

added theorem upperCentralSeries.eq_ge_of_eq_succ

added theorem upperCentralSeries.eq_top