Theorem CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle

Modification history

2024-02-10 12:15
Mathlib/CategoryTheory/Bicategory/Adjunction.lean
feat(Bicategory/Adjunction): the left triangle implies the right triangle for equivalences (#10398)
Added CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangleView on Github →