Commit 2023-05-27 20:20 9b8711f0

View on Github →

feat: port Algebra.Category.ModuleCat.Monoidal.Basic (#4368)

Estimated changes

Modified Mathlib.lean

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

added def ModuleCat.MonoidalCategory.associator

added theorem ModuleCat.MonoidalCategory.associator_hom_apply

added theorem ModuleCat.MonoidalCategory.associator_inv_apply

added theorem ModuleCat.MonoidalCategory.associator_naturality

added theorem ModuleCat.MonoidalCategory.hom_apply

added def ModuleCat.MonoidalCategory.leftUnitor

added theorem ModuleCat.MonoidalCategory.leftUnitor_hom_apply

added theorem ModuleCat.MonoidalCategory.leftUnitor_inv_apply

added theorem ModuleCat.MonoidalCategory.leftUnitor_naturality

added theorem ModuleCat.MonoidalCategory.pentagon

added def ModuleCat.MonoidalCategory.rightUnitor

added theorem ModuleCat.MonoidalCategory.rightUnitor_hom_apply

added theorem ModuleCat.MonoidalCategory.rightUnitor_inv_apply

added theorem ModuleCat.MonoidalCategory.rightUnitor_naturality

added def ModuleCat.MonoidalCategory.tensorHom

added def ModuleCat.MonoidalCategory.tensorObj

added theorem ModuleCat.MonoidalCategory.tensor_comp

added theorem ModuleCat.MonoidalCategory.tensor_id

added theorem ModuleCat.MonoidalCategory.triangle