# mathlibdocumentation

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

• polynomial.chebyshev₁_mul, the (m * n)-th Chebyshev polynomial is the composition of the m-th and n-th Chebyshev polynomials.
• polynomial.lambdashev_mul, the (m * n)-th lambdashev polynomial is the composition of the m-th and n-th lambdashev polynomials.
• polynomial.lambdashev_char_p, for a prime number p, the p-th lambdashev polynomial is congruent to X ^ p modulo p.

## 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.

theorem polynomial.chebyshev₁_mul (R : Type u_1) [comm_ring R] (m n : ) :
(m * n) = .comp

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 : ) :
polynomial.eval (x + y) = x ^ n + y ^ n

theorem polynomial.lambdashev_mul (R : Type u_1) [comm_ring R] (m n : ) :
(m * n) = .comp

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

theorem polynomial.lambdashev_comp_comm (R : Type u_1) [comm_ring R] (m n : ) :

theorem polynomial.lambdashev_char_p (R : Type u_1) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] :