English
If x+y ≠ 0, then the degree of the sum equals the degree of the numerator ps plus qr over the common denominator: intDegree(x+y) = natDegree(x.num*y.denom + x.denom*y.num) − natDegree(x.denom*y.denom).
Русский
Если x+y ≠ 0, то степень суммы равна степени числителя ps+qr над общим знаменателем: intDegree(x+y) = natDegree(x.num*y.denom + x.denom*y.num) − natDegree(x.denom*y.denom).
LaTeX
$$$\\text{If } x+y \\neq 0:\\quad \\operatorname{intDegree}(x+y) = \\operatorname{natDegree}(x.num \\cdot y.denom + x.denom \\cdot y.num) - \\operatorname{natDegree}(x.denom \\cdot y.denom)$$$
Lean4
theorem intDegree_add {x y : RatFunc K} (hxy : x + y ≠ 0) :
(x + y).intDegree = (x.num * y.denom + x.denom * y.num).natDegree - (x.denom * y.denom).natDegree :=
natDegree_sub_eq_of_prod_eq (num_ne_zero hxy) (x + y).denom_ne_zero (num_mul_denom_add_denom_mul_num_ne_zero hxy)
(mul_ne_zero x.denom_ne_zero y.denom_ne_zero) (num_denom_add x y)
