mathlib

83bc6634 - feat(category_theory/monoidal): skeleton of a monoidal category is a monoid (#6444)