Def CategoryTheory.Functor.chosenProd.isLimit

Modification history

2026-03-07 22:58
Mathlib/CategoryTheory/Monoidal/Cartesian/FunctorCategory.lean
chore: refactor `CartesianMonoidalCategory` instance on functors (#36331) …
Deleted CategoryTheory.Functor.chosenProd.isLimitView on Github →
2025-03-17 20:55
Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
chore(CategoryTheory/ChosenFiniteProducts/FunctorCategory): remove `noncomputable` (#23022)
Added CategoryTheory.Functor.chosenProd.isLimitView on Github →