Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.equiv_of_fully_faithful_symm_apply

Modification history

2022-04-09 12:31
src/category_theory/functor/fully_faithful.lean
feat(category_theory/faithful): map_iso_injective (#13263)
Deleted category_theory.equiv_of_fully_faithful_symm_applyView on Github →
2020-08-23 23:56
src/category_theory/fully_faithful.lean
feat(category_theory/fully_faithful): equivalence of homsets (#3923) …
Added category_theory.equiv_of_fully_faithful_symm_applyView on Github →