add_def — Mathlib

English

Let q = n1/d1 and r = n2/d2 be nonnegative rationals in reduced form. Then q + r equals (n1 d2 + n2 d1) / (d1 d2) (in reduced form).

Русский

Пусть q = n1/d1 и r = n2/d2 — неотрицательные рациональные числа в несократимом виде. Тогда q + r равно (n1 d2 + n2 d1) / (d1 d2) (после сокращения).

LaTeX

$$$q + r = \dfrac{q.num \cdot r.den + r.num \cdot q.den}{q.den \cdot r.den}$$$

Lean4

theorem add_def (q r : ℚ≥0) : q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den) := by ext;
  simp [Rat.add_def', Rat.mkRat_eq_divInt, num_coe, den_coe]

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