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.
See the file
ring_theory.polynomial.chebyshev.basic for more properties.
polynomial.chebyshev₁: the Chebyshev polynomials of the first kind.
polynomial.lambdashev: a variant on the Chebyshev polynomials that define a Lambda structure on
In this file we only give definitions and some very elementary simp-lemmas.
This way, we can import this file in
and import that file in turn, in
Add Chebyshev polynomials of the second kind.
chebyshev₁ n is the
n-th Chebyshev polynomial of the first kind