Commit 2023-06-16 00:58 07832160

View on Github →

feat: port CategoryTheory.Monoidal.Internal.FunctorCategory (#5093)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean

added def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso

added def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor

added def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse

added def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Functor.obj

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Inverse.obj

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso

added def CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence

added def CategoryTheory.Monoidal.monFunctorCategoryEquivalence