Theorem Polynomial.Chebyshev.complex_ofReal_eval_C

Modification history

2024-12-20 11:52
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
feat: `aeval` a Chebyshev polynomial (#19952) …
Added Polynomial.Chebyshev.complex_ofReal_eval_CView on Github →