Commit 2023-06-05 08:38 45154842

View on Github →

feat: port Algebra.Category.Module.Monoidal.Symmetric (#4664)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

added theorem ModuleCat.MonoidalCategory.braiding_hom_apply

added theorem ModuleCat.MonoidalCategory.braiding_inv_apply

added theorem ModuleCat.MonoidalCategory.braiding_naturality

added theorem ModuleCat.MonoidalCategory.hexagon_forward

added theorem ModuleCat.MonoidalCategory.hexagon_reverse

added def ModuleCat.braiding