mathlib documentation

ring_theory.polynomial.chebyshev

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

TODO #

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

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

Equations
@[simp]
theorem polynomial.chebyshev.T_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 : ) :
def polynomial.chebyshev.U (R : Type u_1) [comm_ring R] :

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

Equations
@[simp]
theorem polynomial.chebyshev.U_zero (R : Type u_1) [comm_ring R] :
@[simp]
@[simp]
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