Numerator and denominator of a rational multiplier between integers

If a' = r * a with a, a' ∈ ℤ and r ∈ ℚ, then the denominator of r divides a and the numerator of r divides a'. This is Mathlib's Rat.den_dvd and Rat.num_dvd for the fraction a' /. a, restated for a rational r given by the relation it satisfies rather than as an explicit quotient, so that it applies with no case split on a = 0 at the point of use. It is what turns a rational scaling between two integral objects into integer divisibilities, as for the scaling (A, B) ↦ (r⁴A, r⁶B) between two integral short Weierstrass equations.

Main results

• Rat.den_dvd_of_intCast_eq_mul_intCast: a' = r * a implies r.den ∣ a.
• Rat.num_dvd_of_intCast_eq_mul_intCast: a' = r * a implies r.num ∣ a'.

theorem Rat.den_dvd_of_intCast_eq_mul_intCast {a a' : ℤ} (r : ℚ) (h : ↑a' = r * ↑a) : ↑r.den ∣ a

The denominator of a rational multiplier between integers divides the multiplicand: if a' = r * a with a, a' integers, then r.den ∣ a.

theorem Rat.num_dvd_of_intCast_eq_mul_intCast {a a' : ℤ} (r : ℚ) (h : ↑a' = r * ↑a) : r.num ∣ a'

The numerator of a rational multiplier between integers divides the result: if a' = r * a with a, a' integers, then r.num ∣ a'.