2021-07-02 19:46
src/category_theory/adjunction/fully_faithful.lean
feat(category_theory/adjunction/fully_faithful): Converses to `unit_is_iso_of_L_fully_faithful` and `counit_is_iso_of_R_fully_faithful` (#8181) …
Added category_theory.L_full_of_unit_is_iso