Theorem CategoryTheory.coe_toHasForget_instFunLike

Modification history

2026-02-06 21:24
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
refactor(CategoryTheory): remove `HasForget` (#34741)
Deleted CategoryTheory.coe_toHasForget_instFunLikeView on Github →
2025-12-13 14:21
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.coe_toHasForget_instFunLikeView on Github →
2025-01-17 18:04
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
feat(Tactic): basic ConcreteCategory support for elementwise (#20811) …
Added CategoryTheory.coe_toHasForget_instFunLikeView on Github →