Unscaled Polynomial Is Monic

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Unscaled Polynomial Is Monic

The leading coefficient of $P_N(x;\theta)$ is $1$.

theorem unscaledPolynomial_monic (N : ℕ) (θ : ℝ) :
    (unscaledPolynomial N θ).leadingCoeff = 1 := by

Proof ▼


  unfold unscaledPolynomial polynomialFromRealRoots
  induction (realProjectionsList N θ) with
  | nil => simp [List.foldr]
  | cons r rs ih =>
    simp only [List.foldr]
    rw [leadingCoeff_mul, leadingCoeff_X_sub_C, ih, mul_one]

Dependencies (uses)

Unscaled Polynomial

Dependents (used by)

Scaled Polynomial Leading Coefficient

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