Commit 2024-05-28 13:39 e41826d6

View on Github →

feat: index Chebyshev polynomials by integers instead of natural numbers (#13133)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean

modified theorem Polynomial.Chebyshev.T_complex_cos

modified theorem Polynomial.Chebyshev.U_complex_cos

modified theorem Polynomial.Chebyshev.aeval_T

modified theorem Polynomial.Chebyshev.aeval_U

modified theorem Polynomial.Chebyshev.algebraMap_eval_T

modified theorem Polynomial.Chebyshev.algebraMap_eval_U

Modified Mathlib/Data/Complex/Exponential.lean

added theorem Complex.sin_add_sin

Modified Mathlib/RingTheory/Polynomial/Chebyshev.lean

added theorem Polynomial.Chebyshev.T_add_one

modified theorem Polynomial.Chebyshev.T_add_two

modified theorem Polynomial.Chebyshev.T_derivative_eq_U

added theorem Polynomial.Chebyshev.T_eq

modified theorem Polynomial.Chebyshev.T_eq_U_sub_X_mul_U

modified theorem Polynomial.Chebyshev.T_eq_X_mul_T_sub_pol_U

modified theorem Polynomial.Chebyshev.T_mul

added theorem Polynomial.Chebyshev.T_natAbs

added theorem Polynomial.Chebyshev.T_neg

added theorem Polynomial.Chebyshev.T_neg_one

added theorem Polynomial.Chebyshev.T_neg_two

deleted theorem Polynomial.Chebyshev.T_of_two_le

added theorem Polynomial.Chebyshev.T_sub_one

added theorem Polynomial.Chebyshev.T_sub_two

modified theorem Polynomial.Chebyshev.T_two

added theorem Polynomial.Chebyshev.U_add_one

modified theorem Polynomial.Chebyshev.U_add_two

added theorem Polynomial.Chebyshev.U_eq

modified theorem Polynomial.Chebyshev.U_eq_X_mul_U_add_T

added theorem Polynomial.Chebyshev.U_neg

added theorem Polynomial.Chebyshev.U_neg_one

added theorem Polynomial.Chebyshev.U_neg_sub_one

added theorem Polynomial.Chebyshev.U_neg_sub_two

added theorem Polynomial.Chebyshev.U_neg_two

deleted theorem Polynomial.Chebyshev.U_of_two_le

added theorem Polynomial.Chebyshev.U_sub_one

added theorem Polynomial.Chebyshev.U_sub_two

modified theorem Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U

modified theorem Polynomial.Chebyshev.map_T

modified theorem Polynomial.Chebyshev.map_U

modified theorem Polynomial.Chebyshev.mul_T

modified theorem Polynomial.Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T

modified theorem Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T

Modified Mathlib/RingTheory/Polynomial/Dickson.lean