Commit 2025-06-22 20:25 4f1603b0

feat(CategoryTheory/Monoidal/Action): monoidal right actions (#25840) We introduce the notion of a right action of a monoidal category C on a category D. This notion is formally conjugate to that of a left action introduced in #25761, and so are every results in this PR. Please refer to #25761 for a more detailed overview of the notion. The notion comes with its set of notations. We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.