Commit 2026-10-17 13:25 a368e225

View on Github →

chore(GroupTheory/Solvable): to_additivize file (#43108) This PR to_additivizes GroupTheory/Solvable.lean.

Estimated changes

Modified Mathlib/GroupTheory/Abelianization/Defs.lean

added theorem Abelianization.commutator_le_ker

deleted theorem Abelianization.commutator_subset_ker

Modified Mathlib/GroupTheory/Commutator/Basic.lean

Modified Mathlib/GroupTheory/Focal.lean

Modified Mathlib/GroupTheory/IsPerfect.lean

modified theorem Group.IsPerfect.derivedSeries_eq_top

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/GroupTheory/Solvable.lean

added def AddSubgroup.derivedSeries

added theorem Group.not_isSolvable_of_mem_derivedSeries

modified theorem IsSimpleGroup.derivedSeries_succ

added def Subgroup.derivedSeries

added theorem Subgroup.derivedSeries_antitone

added theorem Subgroup.derivedSeries_le_map_derivedSeries

added theorem Subgroup.derivedSeries_normal

added theorem Subgroup.derivedSeries_one

added theorem Subgroup.derivedSeries_succ

added theorem Subgroup.derivedSeries_zero

added theorem Subgroup.map_derivedSeries_eq

added theorem Subgroup.map_derivedSeries_le_derivedSeries

deleted def derivedSeries

deleted theorem derivedSeries_antitone

deleted theorem derivedSeries_le_map_derivedSeries

deleted theorem derivedSeries_normal

deleted theorem derivedSeries_one

deleted theorem derivedSeries_succ

deleted theorem derivedSeries_zero

deleted theorem map_derivedSeries_eq

deleted theorem map_derivedSeries_le_derivedSeries

deleted theorem not_isSolvable_of_mem_derivedSeries

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean