Polynomial from Real Roots
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core
Statement
Given a list of real numbers $[r_1, r_2, \ldots, r_n]$, form the monic polynomial $\prod_{i=1}^{n}(X - r_i)$. This is the unique monic polynomial of degree $n$ having exactly those roots (counted with multiplicity).
def polynomialFromRealRoots (roots : List ℝ) : Polynomial ℝ :=
roots.foldr (fun r p => (X - C r) * p) 1
Dependencies (uses)
NoneNeighborhood
Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms