exists_gcd_one' — Mathlib

English

For integers x,y, there exist integers m',n' with gcd(m',n') = 1 and m = m'·gcd(x,y), n = n'·gcd(x,y).

Русский

Для целых x,y существуют целые m',n' такие, что gcd(m',n') = 1 и m = m'·gcd(x,y), n = n'·gcd(x,y).

LaTeX

$$$$\\exists m',n'\\in\\mathbb{Z},\\; \\gcd(m',n') = 1 \\wedge m = m'\\cdot \\gcd(m,n) \\wedge n = n'\\cdot \\gcd(m,n).$$$$

Lean4

theorem exists_gcd_one' {m n : ℤ} (H : 0 < gcd m n) :
    ∃ (g : ℕ) (m' n' : ℤ), 0 < g ∧ gcd m' n' = 1 ∧ m = m' * g ∧ n = n' * g :=
  let ⟨m', n', h⟩ := exists_gcd_one H
  ⟨_, m', n', H, h⟩

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