mathlib

0026ed93 - feat(category_theory/monoidal/subcategory): monoidal closed structure on full subcategories (#15703)

feat(category_theory/monoidal/subcategory): monoidal closed structure on full subcategories (#15703) I made `monoidal_closed_of_left_rigid_category` a `def` because having it an instance causes diamonds with `full_monoidal_closed_subcategory` or `category_theory.monoidal_closed.functor_category` from #15643. In practice, I think that we rarely want to deduce that a category is monoidal closed from the rigid structure.