mathlib

5b8bb9b4 - feat(category_theory/monoidal): define monoidal structure on the category of monoids in a braided monoidal category (#13122)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>