Commit 2021-03-02 19:27 0c5b5172
View on Github →feat(ring_theory/polynomial/chebyshev/basic): multiplication of Chebyshev polynomials (#6501) Add the identity for multiplication of Chebyshev polynomials,
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.