Commit 2026-06-02 11:20 1cfb3491

View on Github →

feat(GroupTheory/Nilpotent): a nontrivial nilpotent group has a nontrivial center (#39950) and a few upperCentralSeries/lowerCentralSeries API lemmas.

Estimated changes

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem Group.IsNilpotent.center_ne_bot

added theorem Group.IsNilpotent.nilpotencyClass_le_one_iff

added theorem Subgroup.lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_top

added theorem Subgroup.lowerCentralSeries_one_eq_bot_iff

modified theorem Subgroup.upperCentralSeries.eq_ge_of_eq_gt

modified theorem Subgroup.upperCentralSeries.eq_top

added theorem Subgroup.upperCentralSeries_one_eq_top_iff