2024-02-22 12:56
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
feat(CategoryTheory/Localization): construction of a localized category using left fractions (#10606) …
Added CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk