### Abstract

The multiple-angle formulas for $\cos$ and $\sin$ state that for any natural number $n$,
the values of $\cos nx$ and $\sin nx$ can be expressed in terms of $\cos x$ and $\sin x$.
To be more precise, there are polynomials $T_n$ and $U_n$ such that $\cos nx = T_n(\cos x)$
and $\sin nx = U_n(\cos x)\sin x$. These are called the *Chebyshev polynomials of the
first and second kind*, respectively.

This entry contains a definition of these two familes of polynomials in Isabelle/HOL
along with some of their most important properties. In particular, it is shown that $T_n$ and $U_n$
are *orthogonal* families of polynomials.

Moreover, we show the well-known result that for any monic polynomial $p$ of degree $n > 0$,
it holds that $\sup_{x\in[-1,1]} |p(x)| \geq 2^{n-1}$, and that this inequality is sharp since
equality holds with $p = 2^{1-n}\, T_n$. This has important consequences in the theory of
function interpolation, since it implies that the roots of $T_n$ (also colled the
*Chebyshev nodes*) are exceptionally well-suited as interpolation nodes.