mathlib documentation

category_theory.monoidal.skeleton

The monoid on the skeleton of a monoidal category #

The skeleton of a monoidal category is a monoid.

If C is monoidal and skeletal, it is a monoid.

Equations
@[instance]

The skeleton of a monoidal category can be viewed as a monoid, where the multiplication is given by the tensor product, and satisfies the monoid axioms since it is a skeleton.

Equations