Commit 2025-11-17 04:47 d2330fe3

View on Github →

chore: golf proofs involving permutations (#31389) This reduces the diff of #27433.

Estimated changes

Modified Mathlib/Algebra/Group/End.lean

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/Data/Fintype/Perm.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

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

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

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

modified theorem Equiv.Perm.set_support_inv_eq

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean