Commit 2025-03-17 20:55 db4c8abb

View on Github →

chore(CategoryTheory/ChosenFiniteProducts/FunctorCategory): remove noncomputable (#23022)

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean

added def CategoryTheory.Functor.chosenProd.isLimit