divInt_div_divInt — Mathlib

English

The division of two rationals equals the cross-multiplied fraction: (n1/d1) ÷ (n2/d2) = (n1·d2) / (d1·n2).

Русский

Деление двух рациональных чисел равно дроби, полученной перемножением числителя на знаменатель и знаменателя на числитель: (n1/d1) ÷ (n2/d2) = (n1·d2) / (d1·n2).

LaTeX

$$$ (n_{1} /. d_{1}) / (n_{2} /. d_{2}) = (n_{1} * d_{2}) /. (d_{1} * n_{2}) $$$

Lean4

@[simp]
theorem divInt_div_divInt (n₁ d₁ n₂ d₂) : (n₁ /. d₁) / (n₂ /. d₂) = (n₁ * d₂) /. (d₁ * n₂) := by
  rw [div_def, inv_divInt, divInt_mul_divInt]

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