PR for mathlib4 pending + thank you

Stream: new members

[Nicolas Rolland]

I have two PR for mathlib4 pending :

15258, 15375

The lifecycle of a PR says that

someone will probably "review" it within a few days

I would like to thank you for this very interesting library.
There are many concepts in category theory which are looking to escape the whiteboard and help programmers !

[Ruben Van de Velde]

I'm afraid that quote is overly optimistic at the moment

[Eric Wieser]

A few tips for you:

• Adding the relevant t- (topic) labels to your PR increases the chance of a reviewer reviewing it
• You can write #15258 and Zulip will link it automatically
• Make sure to follow the commit convention, which wants every PR description to start with feat:, chore:, refactor:, etc. Hopefully the document describing it in full is easy enough to find from the contribution guide

[Andrew Yang]

I see that you have put feat(CategoryTheory/Monoidal): in the commit message. Please move / copy it into the title as well.

[Daniel Weber]

Also note that there is #PR reviews for this