Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 11:47 5a876cab

View on Github →

feat(category_theory): monoidal_category (C ⥤ C) (#3557)

Estimated changes

Created src/category_theory/monoidal/End.lean

added def category_theory.endofunctor_monoidal_category

added def category_theory.tensoring_right_monoidal

Modified src/category_theory/monoidal/category.lean

added def category_theory.monoidal_category.tensoring_right

Modified src/category_theory/monoidal/functor.lean

added theorem category_theory.monoidal_functor.map_left_unitor

added theorem category_theory.monoidal_functor.map_right_unitor

added theorem category_theory.monoidal_functor.map_tensor