Commit 2026-05-04 16:33 30c8ab11

View on Github →

feat: subtraction and ±1 lemmas for IsCoprime, IsRelPrime (#36948) For both IsCoprime and IsRelPrime we add subtraction variants of the lemmas add_mul_left_left_iff and relatives, as well as specialisations to when 1 is added or subtracted (add_one_left_of_dvd, etc.) and add_one_sub_one_of_two_dvd. We mark all 32 relatives of add_mul_left_left_iff as @[simp]. From my Redhill PhD project.

Estimated changes

Modified Mathlib/RingTheory/Coprime/Basic.lean

modified theorem IsCoprime.add_mul_left_left_iff

modified theorem IsCoprime.add_mul_left_right_iff

modified theorem IsCoprime.add_mul_right_left_iff

modified theorem IsCoprime.add_mul_right_right_iff

added theorem IsCoprime.add_one_left_of_dvd

added theorem IsCoprime.add_one_right_of_dvd

added theorem IsCoprime.add_one_sub_one_of_two_dvd

modified theorem IsCoprime.mul_add_left_left_iff

modified theorem IsCoprime.mul_add_left_right_iff

modified theorem IsCoprime.mul_add_right_left_iff

modified theorem IsCoprime.mul_add_right_right_iff

added theorem IsCoprime.mul_sub_left_left_iff

added theorem IsCoprime.mul_sub_left_right_iff

added theorem IsCoprime.mul_sub_right_left_iff

added theorem IsCoprime.mul_sub_right_right_iff

added theorem IsCoprime.sub_mul_left_left_iff

added theorem IsCoprime.sub_mul_left_right_iff

added theorem IsCoprime.sub_mul_right_left_iff

added theorem IsCoprime.sub_mul_right_right_iff

added theorem IsCoprime.sub_one_left_of_dvd

added theorem IsCoprime.sub_one_right_of_dvd

modified theorem IsRelPrime.add_mul_left_left_iff

modified theorem IsRelPrime.add_mul_left_right_iff

modified theorem IsRelPrime.add_mul_right_left_iff

modified theorem IsRelPrime.add_mul_right_right_iff

added theorem IsRelPrime.add_one_left_of_dvd

added theorem IsRelPrime.add_one_right_of_dvd

added theorem IsRelPrime.add_one_sub_one_of_two_dvd

modified theorem IsRelPrime.mul_add_left_left_iff

modified theorem IsRelPrime.mul_add_left_right_iff

modified theorem IsRelPrime.mul_add_right_left_iff

modified theorem IsRelPrime.mul_add_right_right_iff

added theorem IsRelPrime.mul_sub_left_left_iff

added theorem IsRelPrime.mul_sub_left_right_iff

added theorem IsRelPrime.mul_sub_right_left_iff

added theorem IsRelPrime.mul_sub_right_right_iff

added theorem IsRelPrime.sub_mul_left_left_iff

added theorem IsRelPrime.sub_mul_left_right_iff

added theorem IsRelPrime.sub_mul_right_left_iff

added theorem IsRelPrime.sub_mul_right_right_iff

added theorem IsRelPrime.sub_one_left_of_dvd

added theorem IsRelPrime.sub_one_right_of_dvd