English
For rationals q1 and q2, the denominator of q1+q2 divides the least common multiple of their denominators; i.e. (q1+q2).den | lcm(q1.den,q2.den).
Русский
Для рациональных q1 и q2 den(q1+q2) делит НОК den(q1) и den(q2).
LaTeX
$$$$ (q_1 + q_2).den \\mid q_1.den.lcm q_2.den $$$$
Lean4
theorem add_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den :=
by
rw [add_def, normalize_eq,
Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _) (Nat.gcd_pos_of_pos_right _ (by simp [Nat.pos_iff_ne_zero])), ←
Nat.gcd_mul_lcm, mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]
refine ⟨?_, dvd_mul_right _ _⟩
rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]
apply Int.dvd_add <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast] <;> [exact Nat.gcd_dvd_right _ _;
exact Nat.gcd_dvd_left _ _]
