mathlib3 documentation

ring_theory.polynomial.chebyshev

Chebyshev polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

noncomputable 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]
noncomputable 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]
@[simp]
@[simp]

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