degree_scaleRoots — Mathlib

English

The degree of scaleRoots(p, s) equals the degree of p.

Русский

Степень(scaleRoots(p, s)) равна степени p.

LaTeX

$$$\deg(\operatorname{scaleRoots}(p, s)) = \deg(p)$$$

Lean4

@[simp]
theorem degree_scaleRoots (p : R[X]) {s : R} : degree (scaleRoots p s) = degree p :=
  by
  haveI := Classical.propDecidable
  by_cases hp : p = 0
  · rw [hp, zero_scaleRoots]
  refine le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree ?_)
  rw [coeff_scaleRoots_natDegree]
  intro h
  have := leadingCoeff_eq_zero.mp h
  contradiction

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