Theorem CategoryTheory.Prod.mkHom_eq

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.mkHom_eq View on Github →