English
Given a rational q and integers n,d with d ≠ 0 and q = n/d, there exists an integer c such that n = c·q.num and d = c·q.den; i.e. numerator-denominator scaling factor exists.
Русский
Для рационального q и целых n,d с d ≠ 0 и q = n/d существует целое c такое, что n = c·q.num и d = c·q.den.
LaTeX
$$$$ \\exists c \\in \\mathbb{Z}, \\; n = c \\cdot q.num \\; \\wedge\\; d = c \\cdot q.den, \\quad q = n/ d. $$$$
Lean4
theorem num_den_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = n /. d) : ∃ c : ℤ, n = c * q.num ∧ d = c * q.den :=
by
obtain rfl | hn := eq_or_ne n 0
· simp [qdf]
have : q.num * d = n * ↑q.den := by
refine (divInt_eq_divInt_iff ?_ hd).mp ?_
· exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
· rwa [num_divInt_den]
have hqdn : q.num ∣ n := by
rw [qdf]
exact Rat.num_dvd _ hd
refine ⟨n / q.num, ?_, ?_⟩
· rw [Int.ediv_mul_cancel hqdn]
· refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this
rw [qdf]
exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)
