English
Let q and r be rationals. Then q + r equals the rational with numerator q.num*r.den + q.den*r.num and denominator q.den*r.den.
Русский
Пусть q и r — рациональные числа. Тогда q + r равно дроби с числителем q.num·r.den + q.den·r.num и знаменателем q.den·r.den.
LaTeX
$$q + r = (q.num * r.den + q.den * r.num) / (q.den * r.den)$$
Lean4
theorem add_num_den (q r : ℚ) : q + r = (q.num * r.den + q.den * r.num : ℤ) /. (↑q.den * ↑r.den : ℤ) :=
by
have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos
have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos
conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]
rw [mul_comm r.num q.den]
