Theorem CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor

Modification history

2025-10-28 23:08
Mathlib/CategoryTheory/Closed/Cartesian.lean
feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …
Added CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functorView on Github →