Polynomial Vanishes at Its Roots

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Polynomial Vanishes at Its Roots

If $r \in \mathrm{roots}$, then $\mathrm{polynomialFromRealRoots}(\mathrm{roots})$ evaluated at $r$ is $0$.

theorem polynomialFromRealRoots_eval_mem (roots : List ℝ) (r : ℝ) (hr : r ∈ roots) :
    (polynomialFromRealRoots roots).eval r = 0 := by

Proof ▼


  induction roots with
  | nil => simp at hr
  | cons r' rs ih =>
    unfold polynomialFromRealRoots
    simp only [List.foldr, eval_mul]
    cases List.mem_cons.mp hr with
    | inl h =>
      rw [h]
      simp [eval_sub, eval_X, eval_C]
    | inr h =>
      simp only [mul_eq_zero]
      right
      exact ih h

Dependencies (uses)

Polynomial from Real Roots

Dependents (used by)

Unscaled Polynomial Vanishes at Projected Roots

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