Theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id

Modification history

2023-05-29 14:57
Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
feat: port CategoryTheory.Monoidal.CoherenceLemmas (#4359) …
Added CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_idView on Github →