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

2025-08-07 16:22

Mathlib/CategoryTheory/Products/Basic.lean

chore: replace `aesop` with `simp` where applicable (#28018)

Modified CategoryTheory.Prod.fac'View 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.fac'View on Github →

2025-02-21 15:59

Mathlib/CategoryTheory/Products/Basic.lean

feat(CategoryTheory/Limits/Fubini): relax `HasLimits` hypotheses (#20570) …

Added CategoryTheory.Prod.fac'View on Github →