Theorems · Theorem · commutative algebra

Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval

∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ) (x : R),
  (1 - x ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n)) =
    (2 * ↑k + 1) * x * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n)) -
      (↑n ^ 2 - ↑k ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))

Defined in

Mathlib.RingTheory.Polynomial.Chebyshev

Cited by

2 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing