mathlib documentation

data.zmod.coprime

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.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.