Theorem CategoryTheory.Functor.essSurj_of_comp_fully_faithful

Modification history

2024-06-06 10:53
Mathlib/CategoryTheory/EssentialImage.lean
feat: mapComposableArrows is essentially surjective for localization functors when there is a calculus of fractions (#13558) …
Added CategoryTheory.Functor.essSurj_of_comp_fully_faithfulView on Github →