Commit 2025-05-14 15:37 7c75d4cf
View on Github →refactor: move the construction of ChosenFiniteProducts from finite products with ChosenFiniteProducts (#24679)
Now that ChosenFiniteProducts extends MonoidalCategory, there is no point having the MonoidalCategory version separate from the ChosenFiniteProducts one.
MonoidalOfChosenFiniteProductsSynonym was described as an auxiliary type, so I simply deleted it without deprecation
From Toric