coprime_of_dvd — Mathlib

English

If no prime k divides m also divides n, then gcd(m,n) = 1.

Русский

Если ни одна простая цифра, делящая m, не делит n, то gcd(m,n) = 1.

LaTeX

$$$\\\\forall m,n, (\\\\forall k, \\\\mathrm{Prime}(k) \\\\rightarrow k \\\\mid m \\\\rightarrow \\\\lnot k \\\\mid n)) \\\\Rightarrow \\\\gcd(m,n)=1$$$

Lean4

theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → ¬k ∣ n) : Coprime m n :=
  by
  rw [coprime_iff_gcd_eq_one]
  by_contra g2
  obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
  apply H p hp <;> apply dvd_trans hpdvd
  · exact gcd_dvd_left _ _
  · exact gcd_dvd_right _ _

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