Mathlib v3 is deprecated. Go to Mathlib v4

Def Mon_.trivial

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_.trivial View on Github →