Commit 2025-06-09 05:02 7deb334c

View on Github →

chore: deprime induction in GroupTheory (#25353)

Estimated changes

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean

Modified Mathlib/GroupTheory/Coxeter/Length.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/MonoidLocalization/GrothendieckGroup.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Order.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/OreLocalization/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/GroupTheory/Perm/List.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/GroupTheory/PresentedGroup.lean

Modified Mathlib/GroupTheory/Solvable.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/GroupTheory/Torsion.lean