Reduced integer solutions to linear congruences

A linear congruence with coefficient coprime to its modulus has a solution in the canonical interval of representatives.

Main results

• Int.exists_nonneg_lt_and_dvd_mul_sub: an integer in [0, m) solving a * r ≡ b (mod m) when a is coprime to m.

theorem Int.exists_nonneg_lt_and_dvd_mul_sub (a b : ℤ) (m : ℕ) (hm_pos : 0 < m) (ham : a.gcd ↑m = 1) : ∃ (r : ℤ), 0 ≤ r ∧ r < ↑m ∧ ↑m ∣ a * r - b

A reduced integer solution to a linear congruence. With a coprime to m there is an r in [0, m) solving a * r ≡ b (mod m).

This is ZMod.exists_dvd_sub_val_mul repackaged from a residue class into its canonical integer representative.