Mathlib Changelog
v4
Changelog
About
Github
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