mathlib

145f1270 - feat(ring_theory/polynomial/chebyshev/defs): Chebyshev polynomials of the second kind (#5793)

feat(ring_theory/polynomial/chebyshev/defs): Chebyshev polynomials of the second kind (#5793) This will define Chebyshev polynomials of the second kind and introduce some basic properties: - [x] Define Chebyshev polynomials of the second kind. - [x] Relate Chebyshev polynomials of the first and second kind through recursive formulae - [x] Prove trigonometric identity regarding Chebyshev polynomials of the second kind - [x] Compute the derivative of the Chebyshev polynomials of the first kind in terms of the Chebyshev polynomials of the second kind. - [x] Compute the derivative of the Chebyshev polynomials of the second kind in terms of the Chebyshev polynomials of the first kind. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>