Theorem Polynomial.Chebyshev.C_two_mul_real_cos

Modification history

2024-12-20 11:52
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
feat: `aeval` a Chebyshev polynomial (#19952) …
Modified Polynomial.Chebyshev.C_two_mul_real_cosView on Github →
2024-12-04 05:49
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
feat: the Chebyshev polynomials C and S (#13195) …
Added Polynomial.Chebyshev.C_two_mul_real_cosView on Github →