English
The degree of the reciprocal of a rational function is the negative of the degree: intDegree(x^{-1}) = -intDegree(x).
Русский
Степень обратной рациональной функции равна отрицательной степени: intDegree(x^{-1}) = -intDegree(x).
LaTeX
$$$\\operatorname{intDegree}(x^{-1}) = -\\operatorname{intDegree}(x)$$$
Lean4
@[simp]
theorem intDegree_inv (x : RatFunc K) : intDegree (x⁻¹) = -intDegree x := by
by_cases hx : x = 0 <;> simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx]