Commit 2023-06-04 08:48 9e1c6b39

View on Github →

feat: port CategoryTheory.Monoidal.FunctorCategory (#4646)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

added def CategoryTheory.Monoidal.FunctorCategory.tensorHom

added def CategoryTheory.Monoidal.FunctorCategory.tensorObj

added theorem CategoryTheory.Monoidal.associator_hom_app

added theorem CategoryTheory.Monoidal.associator_inv_app

added theorem CategoryTheory.Monoidal.leftUnitor_hom_app

added theorem CategoryTheory.Monoidal.leftUnitor_inv_app

added theorem CategoryTheory.Monoidal.rightUnitor_hom_app

added theorem CategoryTheory.Monoidal.rightUnitor_inv_app

added theorem CategoryTheory.Monoidal.tensorHom_app

added theorem CategoryTheory.Monoidal.tensorObj_map

added theorem CategoryTheory.Monoidal.tensorObj_obj

added theorem CategoryTheory.Monoidal.tensorUnit_map

added theorem CategoryTheory.Monoidal.tensorUnit_obj