[Merged by Bors] - feat(category_theory/monoidal): skeleton of a monoidal category is a monoid

[b-mehta]

---

cc: @kbuzzard - this is the monoid on the isomorphism classes of a monoidal category you were talking about, and I've put a todo for the commutative monoid when the category is braided

• depends on: [Merged by Bors] - feat(category_theory/monoidal): construct the monoidal inverse to a functor #6442
• depends on: [Merged by Bors] - feat(category_theory/skeletal): skeleton of a general category #6443

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(category_theory/monoidal): construct the monoidal inverse to a functor #6442
• [Merged by Bors] - feat(category_theory/skeletal): skeleton of a general category #6443

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[b-mehta]

@bryangingechen Is it expected that the tick-box in the original message isn't ticked but the dependent PRs are merged?

[bryangingechen]

@bryangingechen Is it expected that the tick-box in the original message isn't ticked but the dependent PRs are merged?

That's a bit weird. Looking at the list of GitHub actions run results, it seems that the "cross of linked issues" task didn't run for #6442, and I don't have any clue why.

In any case it's just a "cosmetic" bug. As you can tell, the "dependent issues bot" was still able to figure out that all the dependencies were merged. I'll check the box in the PR comment now.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests