isCoprime_iff_coprime — Mathlib

English

If a and b are coprime as naturals, then their images in any commutative ring R are coprime.

Русский

Если натуральные числа a и b взаимно просты, то их изображение в любом коммутативном кольце R взаимно просты.

LaTeX

$$$a\text{ and }b\ \text{coprime} \implies IsCoprime\ (a: R)\ (b: R)$$$

Lean4

@[simp, norm_cast]
theorem isCoprime_iff_coprime {m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.Coprime m n := by
  rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]

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