Theorem CategoryTheory.coe_toHasForget_instFunLike

Modification history

2025-01-17 18:04

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

feat(Tactic): basic ConcreteCategory support for elementwise (#20811) …

Added CategoryTheory.coe_toHasForget_instFunLike View on Github →