Theorem EquivLike.apply_inv_apply

Modification history

2025-07-04 03:07

Mathlib/Data/FunLike/Equiv.lean

fix: remove explicit `FunLike` instance for `Equiv` (#26220) …

Modified EquivLike.apply_inv_apply View on Github →

2022-11-10 22:45

Mathlib/Data/FunLike/Equiv.lean

feat: port of Data.FunLike (#541) …

Added EquivLike.apply_inv_apply View on Github →