Polynomial Vanishes at Zero Iff Zero Is a Root

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Polynomial Vanishes at Zero Iff Zero Is a Root
[blueprint]

$\mathrm{polynomialFromRealRoots}(\mathrm{roots})(0) = 0 \iff 0 \in \mathrm{roots}.$

theorem polynomialFromRealRoots_eval_zero_iff_mem_zero (roots : List ℝ) :
    (polynomialFromRealRoots roots).eval 0 = 0 ↔ 0 ∈ roots := by
Proof ▼ 


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

Dependencies (uses)

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms