Theorem CategoryTheory.forget_eq_ConcreteCategory_hom

Modification history

2025-01-17 15:43
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) …
Added CategoryTheory.forget_eq_ConcreteCategory_homView on Github →