exists_gcd_one — Mathlib

English

If gcd(m,n) > 0, there exist integers m', n' such that gcd(m',n') = 1 and m = m'·gcd(m,n), n = n'·gcd(m,n).

Русский

Если gcd(m,n) > 0, существуют целые m', n' такие, что gcd(m',n') = 1 и m = m'·gcd(m,n), n = n'·gcd(m,n).

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) : ∃ m' n' : ℤ, gcd m' n' = 1 ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
  ⟨_, _, gcd_div_gcd_div_gcd H, (Int.ediv_mul_cancel (gcd_dvd_left ..)).symm,
    (Int.ediv_mul_cancel (gcd_dvd_right ..)).symm⟩

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