English
For q1, q2 ∈ ℚ≥0, the product of numerators satisfies q1.num · q2.num = (q1 q2).num · gcd(q1.num · q2.num, q1.den · q2.den).
Русский
Пусть q1, q2 ∈ ℚ≥0. Тогда произведение числителей равно (q1 q2).num · gcd(q1.num · q2.num, q1.den · q2.den).
LaTeX
$$$\\\\forall q_1,q_2 \\\\in \\\\mathbb{Q}_{\\\\ge 0}, \\\\ q_1.\\\\mathrm{num} \\\\cdot q_2.\\\\mathrm{num} = (q_1 q_2).\\\\mathrm{num} \\\\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_num` without division. -/
theorem num_mul_num_eq_num_mul_gcd (q₁ q₂ : ℚ≥0) :
q₁.num * q₂.num = (q₁ * q₂).num * ((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) :=
by
zify
convert Rat.num_mul_num_eq_num_mul_gcd q₁ q₂ <;> norm_cast
