Theorem CategoryTheory.forget_obj

Modification history

2025-07-01 00:55

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

chore: bump toolchain to v4.22.0-rc2 (#26564) …

Modified CategoryTheory.forget_obj View on Github →

2025-01-17 15:43

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) …

Added CategoryTheory.forget_obj View on Github →