Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Mon_.Mon_tensor_mul_one

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_.Mon_tensor_mul_oneView on Github →