Mathlib Changelog
v4
Changelog
About
Github
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.isLimit
View on Github →
2025-03-17 20:55
Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
chore(CategoryTheory/ChosenFiniteProducts/FunctorCategory): remove `noncomputable` (#23022)
Added
CategoryTheory.Functor.chosenProd.isLimit
View on Github →