Def CategoryTheory.ConcreteCategory.instFunLike

Modification history

2024-05-07 01:05

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted CategoryTheory.ConcreteCategory.instFunLike View on Github →

2024-01-19 09:25

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

refactor(*): abbreviation for non-dependent `FunLike` (#9833) …

Added CategoryTheory.ConcreteCategory.instFunLike View on Github →