mathlib4
mathlib4 copied to clipboard
feat(Category/Theory/Monoidal): monoids in a symmetric category form a symmetric category