English
For q1, q2 ∈ ℚ≥0, the equality q1.den · q2.den = (q1 q2).den · gcd(q1.num · q2.num, q1.den · q2.den) holds.
Русский
Пусть q1, q2 ∈ ℚ≥0. Тогда q1.den · q2.den = (q1 q2).den · gcd(q1.num · q2.num, q1.den · q2.den).
LaTeX
$$$\\\\forall q_1,q_2 \\\\in \\\\mathbb{Q}_{\\\\ge 0}, \\\\ q_1.\\\\mathrm{den} \\\\cdot q_2.\\\\mathrm{den} = (q_1 q_2).\\\\mathrm{den} \\\\cdot \\gcd(q_1.\\\\mathrm{num} \\\\cdot q_2.\\\\mathrm{num}, q_1.\\\\mathrm{den} \\\\cdot q_2.\\\\mathrm{den}).$$$
Lean4
/-- A version of `NNRat.mul_den` without division. -/
theorem den_mul_den_eq_den_mul_gcd (q₁ q₂ : ℚ≥0) :
q₁.den * q₂.den = (q₁ * q₂).den * ((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) :=
by
convert Rat.den_mul_den_eq_den_mul_gcd q₁ q₂
norm_cast
