Commit 2025-07-04 03:07 40cb750f

View on Github →

fix: remove explicit FunLike instance for Equiv (#26220) Remove explicit FunLike instance for Equiv. It can already be inferred from the EquivLike instance.

Estimated changes

Modified Mathlib/Algebra/Category/AlgCat/Limits.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

Modified Mathlib/Algebra/Category/Ring/Limits.lean

Modified Mathlib/Data/FunLike/Equiv.lean

modified theorem EquivLike.apply_inv_apply

added theorem EquivLike.coe_apply

modified theorem EquivLike.inv_apply_apply

added theorem EquivLike.inv_apply_eq

modified theorem EquivLike.inv_apply_eq_iff_eq_apply

Modified Mathlib/Logic/Equiv/Defs.lean

added def Equiv.instFunLike

Modified Mathlib/Order/Interval/Finset/Defs.lean