coprime_iff_not_dvd — Mathlib

English

If p is prime, then p and n are coprime exactly when p does not divide n.

Русский

Для простого p верно: p и n взаимно просты тогда и только тогда, когда p не делит n.

LaTeX

$$$\\\\forall p,n \\\\in \\\\mathbb{N}, \\\\mathrm{Prime}(p) \\\\rightarrow (\\\\gcd(p,n)=1 \\\\Leftrightarrow \\\\lnot p \\\\mid n)$$$

Lean4

theorem coprime_iff_not_dvd {p n : ℕ} (pp : Prime p) : Coprime p n ↔ ¬p ∣ n :=
  ⟨fun co d => pp.not_dvd_one <| co.dvd_of_dvd_mul_left (by simp [d]), fun nd =>
    coprime_of_dvd fun _ m2 mp => ((prime_dvd_prime_iff_eq m2 pp).1 mp).symm ▸ nd⟩

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