Theorem Bicategory.Opposite.op2_leftUnitor_inv

Modification history

2025-11-04 09:42
Mathlib/CategoryTheory/Bicategory/Opposites.lean
feat(Bicategory/Opposites): add 1-cell opposite bicategory (#25901) …
Added Bicategory.Opposite.op2_leftUnitor_invView on Github →