Monoids as discrete monoidal categories #
The discrete category on a monoid is a monoidal category. Multiplicative morphisms induced monoidal functors.
@[simp]
@[simp]
The discrete category on a monoid is a monoidal category. Multiplicative morphisms induced monoidal functors.