Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-19 04:51 567954fa

View on Github →

feat(category_theory): lim : (J ⥤ C) ⥤ C is lax monoidal when C is monoidal (#4132) A step towards constructing limits in Mon_ C (and thence towards sheaves of modules as internal objects).

Estimated changes