Commit 2025-01-31 17:41 47acb746

feat(CategoryTheory): the monoidal category structure on a localization (#20951) In #12728, we shall show that if C is a monoidal category and W is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal. In this PR, we only define the MonoidalCategoryStruct instance and check the easy compatibilities. The pentagon and the triangle identities will be done in the separate PR #12728.