coprime_of_dvd' — Mathlib

English

If for every prime k, k divides m and n implies k divides 1, then gcd(m,n) = 1.

Русский

Если для каждого простого k из условия следует, что k делит m и n, тогда k делит 1, то gcd(m,n) = 1.

LaTeX

$$$$ \left( \forall k, \operatorname{Prime}(k) \rightarrow (k \mid m \land k \mid n \Rightarrow k \mid 1) \right) \Rightarrow \gcd(m,n) = 1. $$$$

Lean4

theorem coprime_of_dvd' {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → k ∣ n → k ∣ 1) : Coprime m n :=
  coprime_of_dvd fun k kp km kn => not_le_of_gt kp.one_lt <| le_of_dvd Nat.one_pos <| H k kp km kn

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