mathlib

9e9dfc26 - feat(category_theory/adjunction/fully_faithful): Converses to `unit_is_iso_of_L_fully_faithful` and `counit_is_iso_of_R_fully_faithful` (#8181)

feat(category_theory/adjunction/fully_faithful): Converses to `unit_is_iso_of_L_fully_faithful` and `counit_is_iso_of_R_fully_faithful` (#8181) Add a converse to `unit_is_iso_of_L_fully_faithful` and to `counit_is_iso_of_R_fully_faithful` Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>