Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Mon_.one_mul_hom

Modification history

2020-09-11 14:46
src/category_theory/monoidal/internal.lean
feat(category_theory/monoidal): lax monoidal functors take monoids to monoids (#4108)
Added Mon_.one_mul_homView on Github →