Coprimality and vanishing

We show that for prime p, the image of an integer a in ZMod p vanishes if and only if a and p are not coprime.

theorem ZMod.coe_int_isUnit_iff_isCoprime (n : ℤ) (m : ℕ) : IsUnit ↑n ↔ IsCoprime (↑m) n

theorem ZMod.eq_zero_iff_gcd_ne_one {a : ℤ} {p : ℕ} [pp : Fact (Nat.Prime p)] : ↑a = 0 ↔ a.gcd ↑p ≠ 1

If p is a prime and a is an integer, then a : ZMod p is zero if and only if gcd a p ≠ 1.

theorem ZMod.ne_zero_of_gcd_eq_one {a : ℤ} {p : ℕ} (pp : Nat.Prime p) (h : a.gcd ↑p = 1) : ↑a ≠ 0

If an integer a and a prime p satisfy gcd a p = 1, then a : ZMod p is nonzero.

theorem ZMod.eq_zero_of_gcd_ne_one {a : ℤ} {p : ℕ} (pp : Nat.Prime p) (h : a.gcd ↑p ≠ 1) : ↑a = 0

If an integer a and a prime p satisfy gcd a p ≠ 1, then a : ZMod p is zero.