Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.limits.lim_lax_obj'

Modification history

2020-09-19 04:51
src/category_theory/monoidal/limits.lean
feat(category_theory): `lim : (J ⥤ C) ⥤ C` is lax monoidal when `C` is monoidal (#4132) …
Added category_theory.limits.lim_lax_obj'View on Github →