ne_zero_of_gcd_eq_one — Mathlib

English

If p is prime and gcd(a, p) = 1, then a ≢ 0 (mod p); equivalently the image of a in ZMod p is nonzero.

Русский

Если p — простое и gcd(a, p) = 1, то a не равен 0 по модулю p.

LaTeX

$$$(a : \mathbb{Z}) \bmod p \neq 0$$$

Lean4

/-- If an integer `a` and a prime `p` satisfy `gcd a p = 1`, then `a : ZMod p` is nonzero. -/
theorem ne_zero_of_gcd_eq_one {a : ℤ} {p : ℕ} (pp : p.Prime) (h : a.gcd p = 1) : (a : ZMod p) ≠ 0 :=
  mt (@eq_zero_iff_gcd_ne_one a p ⟨pp⟩).mp (Classical.not_not.mpr h)

Похожие утверждения