A primitive common denominator of two rationals

For rationals x and y there is an integer a clearing both denominators, a x = b and a y = c with b, c ∈ ℤ, such that the triple (a, b, c) is primitive: some integer combination of a, b and c equals 1. Applied to the coefficients of a monic rational quadratic t² = x t + y, it rescales the relation to a primitive integral one a t² - b t - c = 0, which is how primitive quadratic equations of irrational numbers enter the theory of lattices in quadratic fields (D. A. Cox, Primes of the Form x² + ny², §7).

The integer a is the common denominator x.den * y.den divided by the greatest common divisor of the three resulting integers.

theorem Rat.exists_primitive_common_denominator (x y : ℚ) : ∃ (a : ℤ), ∃ (b : ℤ), ∃ (c : ℤ), ↑a * x = ↑b ∧ ↑a * y = ↑c ∧ ∃ (u : ℤ), ∃ (v : ℤ), ∃ (w : ℤ), u * a + v * b + w * c = 1

A primitive common denominator. For rationals x and y there are integers a, b, c with a x = b and a y = c such that a, b and c generate the unit ideal of ℤ.