Theorem CategoryTheory.hom_comp

Modification history

2026-02-06 21:24

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

refactor(CategoryTheory): remove `HasForget` (#34741)

Modified CategoryTheory.hom_comp View on Github →

2025-01-17 15:43

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

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

Added CategoryTheory.hom_comp View on Github →