Commit 2023-03-18 20:50 8037968d

View on Github →

feat: port RingTheory.Polynomial.Chebyshev (#2880)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

added theorem Polynomial.derivative_ofNat

Modified Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.ofNat_comp

Created Mathlib/RingTheory/Polynomial/Chebyshev.lean

added theorem Polynomial.Chebyshev.T_add_two

added theorem Polynomial.Chebyshev.T_derivative_eq_U

added theorem Polynomial.Chebyshev.T_eq_U_sub_X_mul_U

added theorem Polynomial.Chebyshev.T_eq_X_mul_T_sub_pol_U

added theorem Polynomial.Chebyshev.T_mul

added theorem Polynomial.Chebyshev.T_of_two_le

added theorem Polynomial.Chebyshev.T_one

added theorem Polynomial.Chebyshev.T_two

added theorem Polynomial.Chebyshev.T_zero

added theorem Polynomial.Chebyshev.U_add_two

added theorem Polynomial.Chebyshev.U_eq_X_mul_U_add_T

added theorem Polynomial.Chebyshev.U_of_two_le

added theorem Polynomial.Chebyshev.U_one

added theorem Polynomial.Chebyshev.U_two

added theorem Polynomial.Chebyshev.U_zero

added theorem Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U

added theorem Polynomial.Chebyshev.map_T

added theorem Polynomial.Chebyshev.map_U

added theorem Polynomial.Chebyshev.mul_T

added theorem Polynomial.Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T

added theorem Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T