Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Mon_.mul_left_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_.mul_left_unitorView on Github →