mathlib documentation


Chebyshev polynomials #

The Chebyshev polynomials are two families of polynomials indexed by , with integral coefficients.

Main definitions #

Main statements #

Implementation details #

Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo p, we define them to have coefficients in an arbitrary commutative ring, even though technically would suffice. The benefit of allowing arbitrary coefficient rings, is that the statements afterwards are clean, and do not have map (int.cast_ring_hom R) interfering all the time.

References #

Lionel Ponton, Roots of the Chebyshev polynomials: A purely algebraic approach


noncomputable def polynomial.chebyshev.T (R : Type u_1) [comm_ring R] :

T n is the n-th Chebyshev polynomial of the first kind

theorem polynomial.chebyshev.T_zero (R : Type u_1) [comm_ring R] :
noncomputable def polynomial.chebyshev.U (R : Type u_1) [comm_ring R] :

U n is the n-th Chebyshev polynomial of the second kind

theorem polynomial.chebyshev.U_zero (R : Type u_1) [comm_ring R] :
theorem polynomial.chebyshev.map_T {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :
theorem polynomial.chebyshev.map_U {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :

The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials.

The (m * n)-th Chebyshev polynomial is the composition of the m-th and n-th