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] :