Theorem ModuleCat.MonoidalCategory.braiding_naturality

Modification history

2025-10-29 04:59
Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
feat(Algebra/Category): symmetric monoidal structure on `SemimoduleCat` (#30638) …
Deleted ModuleCat.MonoidalCategory.braiding_naturalityView on Github →
2023-06-05 08:38
Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
feat: port Algebra.Category.Module.Monoidal.Symmetric (#4664)
Added ModuleCat.MonoidalCategory.braiding_naturalityView on Github →