Commit 2024-11-19 17:06 ee430423

View on Github →

feat: define instances of Finite, Fintype, DecidableEq for MulEquiv (#17057)

Estimated changes

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

added theorem MulEquiv.toEquiv_injective

Modified Mathlib/Data/Finite/Prod.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Fintype/Perm.lean