intDegree_inv — Mathlib

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]

Похожие утверждения