mathlib3

bae02292 - feat(category_theory/monoidal/subcategory): full monoidal subcategories (#14311)

feat(category_theory/monoidal/subcategory): full monoidal subcategories (#14311) We use a type synonym for `{X : C // P X}` when `C` is a monoidal category and the property `P` is closed under the monoidal unit and tensor product so that `full_monoidal_subcategory` can be made an instance. Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>