Commit 2025-06-02 17:11 c8e33dbb

View on Github →

feat(GroupTheory): Add some results about derivedSeries (#25342) Prove Antitone (derivedSeries G) and (derivedSeries G n).Characteristic.

Estimated changes

Modified Mathlib/GroupTheory/Abelianization.lean

added theorem Subgroup.commutator_le_self

Modified Mathlib/GroupTheory/Solvable.lean

added theorem derivedSeries_antitone