Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-13 07:30 5b8bb9b4

View on Github →

feat(category_theory/monoidal): define monoidal structure on the category of monoids in a braided monoidal category (#13122) Building on the preliminary work from the previous PRs, we finally show that monoids in a braided monoidal category form a monoidal category.

Estimated changes