isCoprime_iff_gcd_eq_one — Mathlib

English

For integers m and n, IsCoprime m n holds exactly when gcd(m, n) = 1.

Русский

Для целых чисел m и n взаимная простота эквивалентна gcd(m, n) = 1.

LaTeX

$$$IsCoprime\ m\ n \iff gcd(m, n) = 1$$$

Lean4

theorem isCoprime_iff_gcd_eq_one {m n : ℤ} : IsCoprime m n ↔ Int.gcd m n = 1 :=
  by
  constructor
  · rintro ⟨a, b, h⟩
    refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)
    rwa [mul_comm m, mul_comm n, eq_comm]
  · rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
    intro h
    exact ⟨_, _, h⟩

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