English
For any integers a,b, the denominator of a/b divides b unless b = 0; more precisely, (a/b).den divides b.
Русский
Для любых a,b целых, знаменатель дроби a/b делится на b (если b ≠ 0).
LaTeX
$$$$ (a /. b).den \\mid b, \\quad b \\neq 0. $$$$
Lean4
theorem den_dvd (a b : ℤ) : ((a /. b).den : ℤ) ∣ b :=
by
by_cases b0 : b = 0; · simp [b0]
rcases e : a /. b with ⟨n, d, h, c⟩
rw [mk'_eq_divInt, divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e
refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_
rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]; simp
