prime_ne_zero — Mathlib

English

If p and q are distinct primes, then q is nonzero modulo p.

Русский

Если p и q — простые числа и p ≠ q, то q не равно нулю по модулю p.

LaTeX

$$$q \\neq 0 \\;\\text{в} \\; \\mathbb{Z}/p\\mathbb{Z} \\;\\text{cuando } p,q \\text{ primes } p \\neq q$$$

Lean4

theorem prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq : p ≠ q) : (q : ZMod p) ≠ 0 := by
  rwa [← Nat.cast_zero, Ne, natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd, ← hp.1.coprime_iff_not_dvd,
    Nat.coprime_primes hp.1 hq.1]

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