Theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv

Modification history

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