div_def' — Mathlib

English

Division in rationals is given by cross-multiplication: q / r = (q.num · r.den) / (q.den · r.num).

Русский

Деление в рациональных числах задаётся через перекрестное умножение: q / r = (q.num · r.den) / (q.den · r.num).

LaTeX

$$$ q / r = (q.num * r.den) /. (q.den * r.num) $$$

Lean4

theorem div_def' (q r : ℚ) : q / r = (q.num * r.den) /. (q.den * r.num) := by
  rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]

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