num_mk — Mathlib

English

For a rational q = n/d, the numerator equals d.sign · n divided by gcd(n,d); i.e. (n/d).num = d.sign·n / gcd(n,d).

Русский

Для рационального q = n/d числитель равен d.sign·n, делённому на gcd(n,d).

LaTeX

$$$$ (n/. d).num = d.sign \\cdot n / n.gcd d, $$$$

Lean4

theorem num_mk (n d : ℤ) : (n /. d).num = d.sign * n / 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.sign, Int.gcd, Int.zero_ediv, this]

Похожие утверждения