intDegree_neg — Mathlib

English

Negating a rational function does not change its degree: intDegree(-x) = intDegree(x).

Русский

Отрицание рациональной функции не изменяет её степень: intDegree(-x) = intDegree(x).

LaTeX

$$$\\operatorname{intDegree}(-x) = \\operatorname{intDegree}(x)$$$

Lean4

@[simp]
theorem intDegree_neg (x : RatFunc K) : intDegree (-x) = intDegree x :=
  by
  by_cases hx : x = 0
  · rw [hx, neg_zero]
  · rw [intDegree, intDegree, ← natDegree_neg x.num]
    exact
      natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
        (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)

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