Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-08 16:51 ab2c6a7b

View on Github →

feat(ring_theory/polynomial/chebyshev): general cleanup (#15799) We move map_T to save on some variables blocks, and clean up some spacing.

Estimated changes

Modified src/ring_theory/polynomial/chebyshev.lean

modified theorem polynomial.chebyshev.T_add_two

modified theorem polynomial.chebyshev.T_derivative_eq_U

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

modified theorem polynomial.chebyshev.T_of_two_le

modified theorem polynomial.chebyshev.T_two

modified theorem polynomial.chebyshev.U_add_two

modified theorem polynomial.chebyshev.U_eq_X_mul_U_add_T

modified theorem polynomial.chebyshev.U_of_two_le

modified theorem polynomial.chebyshev.U_two

modified theorem polynomial.chebyshev.map_T

modified theorem polynomial.chebyshev.map_U

modified theorem polynomial.chebyshev.mul_T