Def CategoryTheory.ConcreteCategory.homEquiv

Modification history

2025-01-17 15:43

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

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

Added CategoryTheory.ConcreteCategory.homEquiv View on Github →