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) …
Deleted CategoryTheory.prod.hom_extView on Github →
2024-10-17 07:12
Mathlib/CategoryTheory/Products/Basic.lean
feat(CategoryTheory/Products): an ext lemma for morphisms in product categories (#17721) …
Added CategoryTheory.prod.hom_extView on Github →