mul_den — Mathlib

English

For rationals q1,q2, the denominator of their product equals q1.den · q2.den divided by gcd of (q1.num · q2.num).natAbs and (q1.den · q2.den).

Русский

Для рационалов q1,q2 знаменатель произведения равен q1.den · q2.den деленному на gcd( |q1.num q2.num|, |q1.den q2.den| ).

LaTeX

$$$$ (q_1 \\cdot q_2).den = \\dfrac{q_1.den \\cdot q_2.den}{ \\gcd( (q_1.num \\cdot q_2.num).natAbs, (q_1.den \\cdot q_2.den) ) }.cast, $$$$

Lean4

theorem mul_den (q₁ q₂ : ℚ) : (q₁ * q₂).den = q₁.den * q₂.den / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den) := by
  rw [mul_def, normalize_eq]

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