Commit 2021-01-29 06:49 145f1270

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:

• Define Chebyshev polynomials of the second kind.
• Relate Chebyshev polynomials of the first and second kind through recursive formulae
• Prove trigonometric identity regarding Chebyshev polynomials of the second kind
• Compute the derivative of the Chebyshev polynomials of the first kind in terms of the Chebyshev polynomials of the second kind.
• Compute the derivative of the Chebyshev polynomials of the second kind in terms of the Chebyshev polynomials of the first kind.