den_mul_den_eq_den_mul_gcd — Mathlib

English

A version of the relation for denominators: the product of denominators equals the product of the rational denominator and a gcd factor of numerators and denominators.

Русский

Версия соотношения знаменателей: произведение знаменателей равно произведению знаменателей и НОД числителей и знаменателей.

LaTeX

$$q₁.den * q₂.den = (q₁ * q₂).den * ((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))$$

Lean4

/-- A version of `Rat.mul_den` without division. -/
theorem den_mul_den_eq_den_mul_gcd (q₁ q₂ : ℚ) :
    q₁.den * q₂.den = (q₁ * q₂).den * ((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) :=
  by
  rw [mul_den]
  exact ((Nat.dvd_iff_div_mul_eq _ _).mp (Nat.gcd_dvd_right _ _)).symm

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