mathlib3 documentation

category_theory.monoidal.skeleton

The monoid on the skeleton of a monoidal category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The skeleton of a monoidal category is a monoid.

@[reducible]

If C is monoidal and skeletal, it is a monoid. See note [reducible non-instances].

Equations
@[protected, 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