mathlib

c994ab3f - feat(category_theory/monoidal): define a monoidal structure on the tensor product functor of a braided monoidal category (#13150)

feat(category_theory/monoidal): define a monoidal structure on the tensor product functor of a braided monoidal category (#13150) Given a braided monoidal category `C`, equip its tensor product functor, viewed as a functor from `C × C` to `C` with a strength that turns it into a monoidal functor. See #13033 for a discussion of the motivation of this definition. (This PR replaces #13034 which was accidentally closed.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>