Degree Equals Number of Roots

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Degree Equals Number of Roots

$\deg\bigl(\mathrm{polynomialFromRealRoots}(\mathrm{roots})\bigr) = \lvert\mathrm{roots}\rvert.$

theorem polynomialFromRealRoots_degree (roots : List ℝ) :
    (polynomialFromRealRoots roots).degree = roots.length := by

Proof ▼


  induction roots with
  | nil => simp [polynomialFromRealRoots]
  | cons r rs ih =>
    unfold polynomialFromRealRoots at ih ⊢
    simp only [List.foldr, List.length_cons]
    rw [degree_mul, degree_X_sub_C, ih]
    norm_cast
    ring

Dependencies (uses)

Polynomial from Real Roots

Dependents (used by)

Unscaled Polynomial Degree

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms