Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-12-27 05:26
e9819624
View on Github →
feat(CategoryTheory): the localized category when there is a left calculus of fractions (
#8921
)
Estimated changes
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
added
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq
added
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q
added
def
CategoryTheory.MorphismProperty.LeftFraction.Localization