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

Estimated changes