Commit 2023-06-07 05:59 ae860a65

View on Github →

feat: port CategoryTheory.Monoidal.Subcategory (#4769)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Subcategory.lean

added def CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map

added def CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion

added theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_map

added theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_obj

added def CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map

added def CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion