intDegree_polynomial — Mathlib

English

The degree of the image of a polynomial p ∈ K[X] in RatFunc K is equal to natDegree(p).

Русский

Степень образа полинома p ∈ K[X] в RatFunc K равна natDegree(p).

LaTeX

$$$\\operatorname{intDegree}(\\mathrm{algebraMap}\\,K[X]\\,(\\mathrm{RatFunc}\\,K)\\,p) = \\operatorname{natDegree}(p)$$$

Lean4

@[simp]
theorem intDegree_polynomial {p : K[X]} : intDegree (algebraMap K[X] (RatFunc K) p) = natDegree p := by
  rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one, Int.ofNat_zero, sub_zero]

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