Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.chebyshev.U_complex_cos

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) …
Modified polynomial.chebyshev.U_complex_cosView on Github →
2021-09-27 04:20
src/analysis/special_functions/trigonometric/basic.lean
refactor(analysis/special_functions/trigonometric): split file (#9340) …
Modified polynomial.chebyshev.U_complex_cosView on Github →
2021-03-06 01:08
src/analysis/special_functions/trigonometric.lean
chore(polynomial/chebyshev): changes names of chebyshev₁ to chebyshev.T and chebyshev₂ to chebyshev.U (#6519) …
Added polynomial.chebyshev.U_complex_cosView on Github →