Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Mon_.one_right_unitor

Modification history

2022-04-13 07:30

src/category_theory/monoidal/Mon_.lean

feat(category_theory/monoidal): define monoidal structure on the category of monoids in a braided monoidal category (#13122) …

Added Mon_.one_right_unitor View on Github →