num_mul_num_eq_num_mul_gcd — Mathlib

English

Let q1 and q2 be rationals. Then q1.num * q2.num = (q1*q2).num * gcd(q1.num*q2.num, q1.den*q2.den).

Русский

Пусть q1 и q2 — рациональные числа. Тогда q1.num * q2.num = (q1*q2).num * gcd(q1.num*q2.num, q1.den*q2.den).

LaTeX

$$$q_1.num \cdot q_2.num = (q_1 \cdot q_2).num \cdot ((q_1.num \cdot q_2.num).natAbs.gcd (q_1.den \cdot q_2.den))$$$

Lean4

/-- A version of `Rat.mul_num` without division. -/
theorem num_mul_num_eq_num_mul_gcd (q₁ q₂ : ℚ) :
    q₁.num * q₂.num = (q₁ * q₂).num * ((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) :=
  by
  rw [mul_num]
  refine (Int.ediv_mul_cancel ?_).symm
  rw [← Int.dvd_natAbs]
  exact Int.ofNat_dvd.mpr (Nat.gcd_dvd_left _ _)

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