Coprimality and vanishing #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.eq_zero_iff_gcd_ne_one {a : ℤ} {p : ℕ} [pp : fact (nat.prime p)] :

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) :

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) :

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