Commit 2022-08-10 15:00 0026ed93

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.