Unscaled Polynomial Degree

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Unscaled Polynomial Degree
[blueprint]

$\deg P_N(x;\theta) = N.$

theorem unscaledPolynomial_degree (N : ℕ) (θ : ℝ) :
    (unscaledPolynomial N θ).degree = N := by
Proof ▼ 


  unfold unscaledPolynomial
  rw [polynomialFromRealRoots_degree, card_realProjectionsList]

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