Theorem CategoryTheory.Prod.hom_ext

Modification history

2025-11-24 17:30

Mathlib/CategoryTheory/Products/Basic.lean

feat(Category/Basic): remove simps projection Hom from `CategoryStruct` (#31943) …

Added CategoryTheory.Prod.hom_ext View on Github →