mul_num — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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