coprime_iff_isRelPrime — Mathlib

English

For natural numbers m, n, Coprime m n holds if and only if IsRelPrime m n.

Русский

Для натуральных чисел m, n утверждение Coprime m n эквивалентно IsRelPrime m n.

LaTeX

$$$\forall m,n \in \mathbb{N}, \operatorname{Coprime}(m,n) \iff \operatorname{IsRelPrime}(m,n)$$$

Lean4

theorem coprime_iff_isRelPrime {m n : ℕ} : m.Coprime n ↔ IsRelPrime m n :=
  by
  simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]
  exact ⟨fun h _ ↦ (h ▸ ·), (dvd_one.mp <| · dvd_rfl)⟩

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