English
For any integers a and b with b ≠ 0, the numerator of the rational a/b divides a.
Русский
Для любых целых a и b ≠ 0 числитель дроби a/b делится на a.
LaTeX
$$$$ (a \\/. b).num \\mid a, \\quad a \\in \\mathbb{Z}, \\; b \\in \\mathbb{Z}, \\; b \\neq 0. $$$$
Lean4
theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a :=
by
rcases e : a /. b with ⟨n, d, h, c⟩
rw [Rat.mk'_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e
refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.dvd_of_dvd_mul_right ?_
have := congr_arg Int.natAbs e
simp only [Int.natAbs_mul, Int.natAbs_natCast] at this; simp [this]
