Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 20:15 67821d26

View on Github →

feat(analysis/special_functions/trigonometric/chebyshev): T_real_cos and U_real_cos (#15798) We prove T_real_cos and U_real_cos matching T_complex_cos and U_complex_cos. We also remove two redundant theorems.

Estimated changes

Modified src/analysis/special_functions/trigonometric/chebyshev.lean

modified theorem polynomial.chebyshev.T_complex_cos

added theorem polynomial.chebyshev.T_real_cos

modified theorem polynomial.chebyshev.U_complex_cos

added theorem polynomial.chebyshev.U_real_cos

added theorem polynomial.chebyshev.aeval_T

added theorem polynomial.chebyshev.aeval_U

added theorem polynomial.chebyshev.algebra_map_eval_T

added theorem polynomial.chebyshev.algebra_map_eval_U

added theorem polynomial.chebyshev.complex_of_real_eval_T

added theorem polynomial.chebyshev.complex_of_real_eval_U

deleted theorem polynomial.chebyshev.cos_nat_mul

deleted theorem polynomial.chebyshev.sin_nat_succ_mul