natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree

English

For x ≠ 0 and any nonzero polynomial s, the integer degree of x equals the difference between natDegrees after multiplying numerator by s and denominator by s: ((x.num * s).natDegree) − ((s * x.denom).natDegree) = x.intDegree.

Русский

При x ≠ 0 и любом ненулевом многочлене s разности степеней после умножения числителя на s и знаменателя на s равны intDegree(x).

LaTeX

$$$x \\neq 0 \\Rightarrow \\forall s \\,(s \\neq 0)\\; ((x.num \\cdot s).natDegree - (s \\cdot x.denom).natDegree) = x.intDegree$$$

Lean4

theorem natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree {x : RatFunc K} (hx : x ≠ 0) {s : K[X]}
    (hs : s ≠ 0) : ((x.num * s).natDegree : ℤ) - (s * x.denom).natDegree = x.intDegree :=
  by
  apply
    natDegree_sub_eq_of_prod_eq (mul_ne_zero (num_ne_zero hx) hs) (mul_ne_zero hs x.denom_ne_zero) (num_ne_zero hx)
      x.denom_ne_zero
  rw [mul_assoc]

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