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