# Multiple angle formulas in terms of Chebyshev polynomials #

This file gives the trigonometric characterizations of Chebyshev polynomials, for both the real (Real.cos) and complex (Complex.cos) cosine.

@[simp]
theorem Polynomial.Chebyshev.aeval_T {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (x : A) (n : ) :
=
@[simp]
theorem Polynomial.Chebyshev.aeval_U {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (x : A) (n : ) :
=
@[simp]
theorem Polynomial.Chebyshev.algebraMap_eval_T {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (x : R) (n : ) :
@[simp]
theorem Polynomial.Chebyshev.algebraMap_eval_U {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (x : R) (n : ) :
@[simp]
@[simp]

### Complex versions #

@[simp]
theorem Polynomial.Chebyshev.T_complex_cos (θ : ) (n : ) :
= Complex.cos (n * θ)

The n-th Chebyshev polynomial of the first kind evaluates on cos θ to the value cos (n * θ).

@[simp]
theorem Polynomial.Chebyshev.U_complex_cos (θ : ) (n : ) :
= Complex.sin ((n + 1) * θ)

The n-th Chebyshev polynomial of the second kind evaluates on cos θ to the value sin ((n + 1) * θ) / sin θ.

### Real versions #

@[simp]
theorem Polynomial.Chebyshev.T_real_cos (θ : ) (n : ) :
= Real.cos (n * θ)

The n-th Chebyshev polynomial of the first kind evaluates on cos θ to the value cos (n * θ).

@[simp]
theorem Polynomial.Chebyshev.U_real_cos (θ : ) (n : ) :
= Real.sin ((n + 1) * θ)

The n-th Chebyshev polynomial of the second kind evaluates on cos θ to the value sin ((n + 1) * θ) / sin θ.