isCoprime_iff_nat_coprime — Mathlib

English

For integers a, b, gcd(a,b) = 1 if and only if gcd(|a|,|b|) = 1; i.e., a and b are coprime precisely when their absolute values are coprime.

Русский

Для целых a и b равенство наибольшего общего делителя gcd(a,b) = 1 эквивалентно gcd(|a|,|b|) = 1; то есть числа a и b взаимно просты тогда и только тогда, когда их абсолютные значения взаимно просты.

LaTeX

$$$\\gcd(a,b) = 1 \\iff \\gcd(|a|,|b|) = 1$.$$

Lean4

theorem isCoprime_iff_nat_coprime {a b : ℤ} : IsCoprime a b ↔ Nat.Coprime a.natAbs b.natAbs := by
  rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]

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