Commit 2023-11-01 07:43 12b7b979

View on Github →

feat(CategoryTheory/Localization): equivalence relation on left fractions (#8055)

Estimated changes

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

added def CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective

added def CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom

added theorem CategoryTheory.MorphismProperty.LeftFraction.comp_eq

added def CategoryTheory.MorphismProperty.LeftFraction.comp₀

added theorem CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel

added theorem CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction

added theorem CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac

added theorem CategoryTheory.MorphismProperty.LeftFractionRel.refl

added theorem CategoryTheory.MorphismProperty.LeftFractionRel.symm

added theorem CategoryTheory.MorphismProperty.LeftFractionRel.trans

added def CategoryTheory.MorphismProperty.LeftFractionRel

added theorem CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction

added theorem CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac

added theorem CategoryTheory.MorphismProperty.equivalenceLeftFractionRel