Commit 2025-05-15 18:47 ae681ea3
View on Github →chore: rename ChosenFiniteProducts to CartesianMonoidalCategory (#24390)
Now that ChosenFiniteProducts extends MonoidalCategory, the name ChosenFiniteProducts is less relevant. CartesianMonoidalCategory is a better name for this class.
From Toric
Estimated changes
added theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.rightUnitor_naturality
added theorem CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison
added theorem CategoryTheory.CartesianMonoidalCategory.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison
deleted theorem CategoryTheory.ChosenFiniteProducts.preservesLimit_empty_of_isIso_terminalComparison