not_coprime_iff_dvd — Mathlib

English

Not Coprime m n iff there exists a prime p with p|m and p|n.

Русский

Не взаимно простые m и n эквивалентно существованию простого p, делящего оба числа.

LaTeX

$$$$ \neg \operatorname{Coprime}(m,n) \iff \exists p, \operatorname{Prime}(p) \land p \mid m \land p \mid n. $$$$

Lean4

theorem not_coprime_iff_dvd {m n : ℕ} : ¬Coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n :=
  by
  apply Iff.intro
  · intro h
    exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩
  · intro h
    obtain ⟨p, hp⟩ := h
    apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2

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