English
For q1, q2 ∈ ℚ≥0, the numerator of q1 q2 is (q1.num · q2.num) divided by gcd(q1.num · q2.num, q1.den · q2.den).
Русский
Пусть q1, q2 ∈ ℚ≥0. Числитель произведения q1 q2 равен (num(q1) · num(q2)) делённому на НОД(num(q1) · num(q2), den(q1) · den(q2)).
LaTeX
$$$\\\\forall q_1,q_2 \\\\in \\\\mathbb{Q}_{\\\\ge 0}, \\\\ (q_1 q_2).\\\\mathrm{num} = (q_1.\\\\mathrm{num} \\\\cdot q_2.\\\\mathrm{num}) / \\\\gcd(q_1.\\\\mathrm{num} \\\\cdot q_2.\\\\mathrm{num}, q_1.\\\\mathrm{den} \\\\cdot q_2.\\\\mathrm{den}).$$$
Lean4
theorem mul_num (q₁ q₂ : ℚ≥0) : (q₁ * q₂).num = q₁.num * q₂.num / Nat.gcd (q₁.num * q₂.num) (q₁.den * q₂.den) :=
by
zify
convert Rat.mul_num q₁ q₂ <;> norm_cast
