Commit 2025-11-20 13:23 555129fb

View on Github →

chore(Data/Int/GCD): review API (#31140) This PR makes a few changes, but they are very linked so a single PR seems easiest:

  • Rename Nat.exists_mul_emod_eq_gcd to Nat.exists_mul_mod_eq_gcd, and Nat.exists_mul_emod_eq_one_of_coprime to Nat.exists_mul_mod_eq_one_of_coprime. This is since the % operator on naturals is only ever named mod, whereas emod is reserved for the % operator on integers.
  • Strengthen the statements of those two to additionally deduce that m < k.
  • Add exists_mul_mod_eq_of_coprime, which is the non-one generalisation of exists_mul_mod_eq_one_of_coprime.

Estimated changes