Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-27 04:25 bae02292

View on Github →

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.

Estimated changes