Commit 2024-08-01 02:49 5745d771

View on Github →

chore: backports for leanprover/lean4#4814 (part 8) (#15349) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean.lean

Modified Mathlib/Algebra/Order/Module/Defs.lean

Modified Mathlib/Algebra/Order/Ring/Cast.lean

Modified Mathlib/CategoryTheory/DifferentialObject.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

modified theorem CategoryTheory.GradedObject.hasMap_comp

modified theorem CategoryTheory.GradedObject.mapMap_comp

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

modified theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk

modified def CategoryTheory.MorphismProperty.LeftFraction.comp₀

modified theorem CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel

modified theorem CategoryTheory.MorphismProperty.LeftFraction.map_compatibility

modified theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq

modified theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq_of_map_eq

modified theorem CategoryTheory.MorphismProperty.equivalenceLeftFractionRel

Modified Mathlib/CategoryTheory/Shift/Basic.lean

Modified Mathlib/CategoryTheory/SmallObject/Iteration.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

modified theorem IsRelPrime.add_mul_left_left

modified theorem IsRelPrime.add_mul_left_right

modified theorem IsRelPrime.add_mul_right_left

modified theorem IsRelPrime.add_mul_right_right

modified theorem IsRelPrime.mul_add_left_left

modified theorem IsRelPrime.mul_add_left_right

modified theorem IsRelPrime.mul_add_right_left

modified theorem IsRelPrime.mul_add_right_right

modified theorem IsRelPrime.neg_left

modified theorem IsRelPrime.neg_right

modified theorem isCoprime_mul_unit_left

modified theorem isCoprime_mul_unit_left_left

modified theorem isCoprime_mul_unit_left_right

modified theorem isCoprime_mul_unit_right

modified theorem isCoprime_mul_unit_right_left

modified theorem isCoprime_mul_unit_right_right