Commit 2025-07-15 08:10 09161bde

View on Github →

chore: golf GroupTheory/ using grind (#26681)

Estimated changes

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean

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

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

Modified Mathlib/GroupTheory/Perm/Support.lean