mathlib documentation

ring_theory.polynomial.chebyshev.basic

Chebyshev polynomials

The Chebyshev polynomials are two families of polynomials indexed by , with integral coefficients. In this file, we only consider Chebyshev polynomials of the first kind.

Main declarations

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.

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

A Lambda structure on polynomial

Mathlib doesn't currently know what a Lambda ring is. But once it does, we can endow polynomial with a Lambda structure in terms of the lambdashev polynomials defined below. There is exactly one other Lambda structure on polynomial in terms of binomial polynomials.

theorem polynomial.lambdashev_eval_add_inv {R : Type u_1} [comm_ring R] (x y : R) (h : x * y = 1) (n : ) :

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