Def CategoryTheory.forget

Modification history

2024-05-07 01:05

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

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

Deleted CategoryTheory.forget View on Github →

2023-06-30 06:08

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

chore: reorder universes in ConcreteCategory (#5605)

Modified CategoryTheory.forget View on Github →

2023-03-07 17:18

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

feat: port CategoryTheory.ConcreteCategory.Basic (#2619)

Added CategoryTheory.forget View on Github →