English
For q1, q2 ∈ ℚ≥0, the denominator of q1 q2 equals (q1.den · q2.den) divided by gcd(q1.num · q2.num, q1.den · q2.den).
Русский
Пусть q1, q2 ∈ ℚ≥0.Знаменатель произведения q1 q2 равен (den(q1) · den(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{den} = (q_1.\\\\mathrm{den} \\\\cdot q_2.\\\\mathrm{den}) / \\\\gcd(q_1.\\\\mathrm{num} \\\\cdot q_2.\\\\mathrm{num}, q_1.\\\\mathrm{den} \\\\cdot q_2.\\\\mathrm{den}).$$$
Lean4
theorem mul_den (q₁ q₂ : ℚ≥0) : (q₁ * q₂).den = q₁.den * q₂.den / Nat.gcd (q₁.num * q₂.num) (q₁.den * q₂.den) :=
by
convert Rat.mul_den q₁ q₂
norm_cast
