mathlib

0c5b5172 - feat(ring_theory/polynomial/chebyshev/basic): multiplication of Chebyshev polynomials (#6501)

feat(ring_theory/polynomial/chebyshev/basic): multiplication of Chebyshev polynomials (#6501) Add the identity for multiplication of Chebyshev polynomials, ```lean 2 * chebyshev₁ R m * chebyshev₁ R (m + k) = chebyshev₁ R (2 * m + k) + chebyshev₁ R k ``` Use this to give a direct proof of the identity `chebyshev₁_mul` for composition of Chebyshev polynomials, replacing the current proof using trig functions. This means that the import `import analysis.special_functions.trigonometric` to the Chebyshev file can be removed.