Theorem CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions
Modification history
2024-06-06 10:53
Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.lean
feat: mapComposableArrows is essentially surjective for localization functors when there is a calculus of fractions (#13558) …
Added CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractionsView on Github →