Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 08:55 ce70305b

View on Github →

feat(category_theory): monoidal_category (C ⥤ D) when D is monoidal (#3571) When C is any category, and D is a monoidal category, there is a natural "pointwise" monoidal structure on C ⥤ D. The initial intended application is tensor product of presheaves.

Estimated changes