Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.inv_map_unit

Modification history

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.inv_map_unit View on Github →