Commit 2024-12-20 11:52 772472af

feat: aeval a Chebyshev polynomial (#19952) The theorem Polynomial.Chebyshev.aeval_T states that if R' is an algebra over R, then aeval x (T R n) = (T R' n).eval x. We move this theorem and the equivalent Polynomial.Chebyshev.algebraMap_eval_T from Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean to Mathlib/RingTheory/Polynomial/Chebyshev.lean. We also add variants of this theorem for the Chebyshev C and S polynomials.