Commit 2025-03-13 15:17 40586dcf

View on Github →

chore: move Equiv.Perm.viaFintypeEmbedding_sign out of Logic/ (#22900) Equiv.Perm.sign is a group-theoretic concept.

Estimated changes

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

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

added theorem Equiv.Perm.viaFintypeEmbedding_sign

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/Logic/Equiv/Fintype.lean

deleted theorem Equiv.Perm.viaFintypeEmbedding_sign

Created MathlibTest/Equiv.lean