exists_coprime_of_gcd_pos — Mathlib

English

If 0 < gcd(a.re, a.im), there exists b with a = gcd(a.re, a.im) · b and IsCoprime b.re b.im.

Русский

Если 0 < gcd(a.re, a.im), существует b such that a = gcd(a.re,a.im) · b и IsCoprime b.re b.im.

LaTeX

$$$\exists b:\ a = (\gcd(a_{\re}, a_{\im}) : \mathbb{Z}) \cdot b \land IsCoprime(b_{\re}, b_{\im})$$$

Lean4

theorem exists_coprime_of_gcd_pos {a : ℤ√d} (hgcd : 0 < Int.gcd a.re a.im) :
    ∃ b : ℤ√d, a = ((Int.gcd a.re a.im : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im :=
  by
  obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd
  rw [mul_comm] at Hre Him
  refine ⟨⟨re, im⟩, ?_, ?_⟩
  · rw [smul_val, ← Hre, ← Him]
  · rw [Int.isCoprime_iff_gcd_eq_one, H1]

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