Def CategoryTheory.ConcreteCategory.funLike

Modification history

2024-01-17 23:23

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

chore(*): rename `FunLike` to `DFunLike` (#9785) …

Deleted CategoryTheory.ConcreteCategory.funLike View on Github →

2023-06-13 00:47

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

feat: change `ConcreteCategory.hasCoeToFun` to `FunLike` (#4693)

Added CategoryTheory.ConcreteCategory.funLike View on Github →