mul_def — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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