English
If x ≠ 0 and y ≠ 0 then the degree of the product equals the sum of the degrees: intDegree(xy) = intDegree(x) + intDegree(y).
Русский
Если x ≠ 0 и y ≠ 0, то deg(xy) = deg(x) + deg(y).
LaTeX
$$$x \\neq 0 \\land y \\neq 0 \\Rightarrow \\operatorname{intDegree}(x y) = \\operatorname{intDegree}(x) + \\operatorname{intDegree}(y)$$$
Lean4
theorem intDegree_mul {x y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0) : intDegree (x * y) = intDegree x + intDegree y :=
by
simp only [intDegree, add_sub, sub_add, sub_sub_eq_add_sub, sub_sub, sub_eq_sub_iff_add_eq_add]
norm_cast
rw [← Polynomial.natDegree_mul x.denom_ne_zero y.denom_ne_zero, ←
Polynomial.natDegree_mul (RatFunc.num_ne_zero (mul_ne_zero hx hy)) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero), ←
Polynomial.natDegree_mul (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy), ←
Polynomial.natDegree_mul (mul_ne_zero (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy)) (x * y).denom_ne_zero,
RatFunc.num_denom_mul]
