ZMod lemmas

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem ZMod.intCast_eq_neg_intCast_of_dvd_add {a b : ℤ} {m : ℕ} (h : ↑m ∣ a + b) : ↑b = -↑a

If m ∣ a + b, then b ≡ -a mod m.

theorem ZMod.isUnit_intCast_of_isCoprime_of_dvd_add {a b : ℤ} {m : ℕ} (hcop : IsCoprime (↑m) a) (h : ↑m ∣ a + b) : IsUnit ↑b

If m is coprime to a and divides a + b, then b is a unit mod m.