Commit 2023-04-06 17:52 9d339228

View on Github →

feat: a/c ≡ b/c mod m/c → a ≡ b mod m (#3259) https://github.com/leanprover-community/mathlib/pull/18119, https://github.com/leanprover-community/mathlib/pull/18666.

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

added theorem CharP.intCast_eq_intCast

deleted theorem CharP.int_cast_eq_int_cast_iff

added theorem CharP.natCast_eq_natCast

deleted theorem eq_iff_modEq_int

Modified Mathlib/Algebra/Ring/Divisibility.lean

added theorem dvd_sub_comm

Modified Mathlib/Data/Int/GCD.lean

added theorem Int.gcd_pos_of_ne_zero_left

added theorem Int.gcd_pos_of_ne_zero_right

deleted theorem Int.gcd_pos_of_non_zero_left

deleted theorem Int.gcd_pos_of_non_zero_right

Modified Mathlib/Data/Int/ModEq.lean

added theorem Int.ModEq.cancel_left_div_gcd

added theorem Int.ModEq.cancel_right_div_gcd

added theorem Int.ModEq.of_div

added theorem Int.add_modEq_left

added theorem Int.add_modEq_right

added theorem Int.modEq_comm

added theorem Int.modEq_neg

added theorem Int.modEq_zero_iff

added theorem Int.neg_modEq_neg

Modified Mathlib/Data/Nat/ModEq.lean

added theorem Nat.ModEq.of_div

Modified Mathlib/Data/Nat/Order/Lemmas.lean

added theorem Nat.le_of_lt_add_of_dvd

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.valMinAbs_natCast_eq_self

added theorem ZMod.valMinAbs_natCast_of_half_lt

added theorem ZMod.valMinAbs_natCast_of_le_half