Theorem CategoryTheory.Prod.fac

Modification history

2025-11-24 17:30
Mathlib/CategoryTheory/Products/Basic.lean
feat(Category/Basic): remove simps projection Hom from `CategoryStruct` (#31943) …
Modified CategoryTheory.Prod.facView on Github →
2025-08-07 16:22
Mathlib/CategoryTheory/Products/Basic.lean
chore: replace `aesop` with `simp` where applicable (#28018)
Modified CategoryTheory.Prod.facView on Github →
2025-06-22 05:59
Mathlib/CategoryTheory/Products/Basic.lean
feat(CategoryTheory/Products/Basic): alternative constructor for morphisms in products (#26206) …
Modified CategoryTheory.Prod.facView on Github →
2025-02-21 15:59
Mathlib/CategoryTheory/Products/Basic.lean
feat(CategoryTheory/Limits/Fubini): relax `HasLimits` hypotheses (#20570) …
Added CategoryTheory.Prod.facView on Github →