mathlib3

7886c27b - feat(category_theory/monoidal): lax monoidal functors take monoids to monoids (#4108)