mathlib documentation

ring_theory.polynomial.chebyshev.defs

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.

See the file ring_theory.polynomial.chebyshev.basic for more properties.

Main declarations

Implementation details

In this file we only give definitions and some very elementary simp-lemmas. This way, we can import this file in analysis.special_functions.trigonometric, and import that file in turn, in ring_theory.polynomial.chebyshev.basic.

TODO

Add Chebyshev polynomials of the second kind.

def polynomial.chebyshev₁ (R : Type u_1) [comm_ring R] :

chebyshev₁ n is the n-th Chebyshev polynomial of the first kind

Equations
@[simp]
theorem polynomial.chebyshev₁_zero (R : Type u_1) [comm_ring R] :

theorem polynomial.map_chebyshev₁ {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :

def polynomial.lambdashev (R : Type u_1) [comm_ring R] :

lambdashev R n is equal to 2 * (chebyshev₁ R n).comp (X / 2). It is a family of polynomials that satisfies lambdashev (zmod p) p = X ^ p, and therefore defines a Lambda structure on polynomial.

Equations
@[simp]
theorem polynomial.lambdashev_zero (R : Type u_1) [comm_ring R] :

theorem polynomial.map_lambdashev {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :