Documentation

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