Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.chebyshev.complex_of_real_eval_U

Modification history

2022-08-10 20:15

src/analysis/special_functions/trigonometric/chebyshev.lean

feat(analysis/special_functions/trigonometric/chebyshev): `T_real_cos` and `U_real_cos` (#15798) …

Added polynomial.chebyshev.complex_of_real_eval_U View on Github →