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.
(m * n)-th Chebyshev polynomial is the composition of the
n-th Chebyshev polynomials.
(m * n)-th lambdashev polynomial is the composition of the
n-th lambdashev polynomials.
polynomial.lambdashev_char_p, for a prime number
p-th lambdashev polynomial is congruent to
X ^ pmodulo
Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo
we define them to have coefficients in an arbitrary commutative ring, even though
ℤ 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.
A Lambda structure on
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.