English
For a rational q = n/d, the denominator is 1 if d = 0, otherwise equals |d| / gcd(|n|,|d|); i.e. (n/d).den = if d = 0 then 1 else |d| / gcd(|n|,|d|).
Русский
Для q = n/d знаменатель равен 1 при d = 0, иначе равен |d| / gcd(|n|,|d|).
LaTeX
$$$$ (n /. d).den = \\begin{cases} 1, & d = 0, \\\\ \\mathrm{natAbs}(d) / \\gcd(n, d), & d \\neq 0. \\end{cases} $$$$
Lean4
theorem den_mk (n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d :=
by
have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]
rcases d with ((_ | _) | _) <;>
simp [divInt, mkRat, Rat.normalize_eq, Int.gcd, if_neg (Nat.cast_add_one_ne_zero _), this]
