mathlib3

44282437 - chore(polynomial/chebyshev): changes names of chebyshev₁ to chebyshev.T and chebyshev₂ to chebyshev.U (#6519)

chore(polynomial/chebyshev): changes names of chebyshev₁ to chebyshev.T and chebyshev₂ to chebyshev.U (#6519) Still have to write here what was changed (will be a long list). More or less this is just search and replace `chebyshev₁` for `chebyshev.T` and `chebyshev₂` for `chebyshev.U`. * `polynomial.chebyshev₁` is now `polynomial.chebyshev.T` * `polynomial.chebyshev₁_zero` is now `polynomial.chebyshev.T_zero` * `polynomial.chebyshev₁_one` is now `polynomial.chebyshev.T_one` * `polynomial.chebyshev₁_two` is now `polynomial.chebyshev.T_two` * `polynomial.chebyshev₁_add_two` is now `polynomial.chebyshev.T_add_two` * `polynomial.chebyshev₁_of_two_le` is now `polynomial.chebyshev.T_of_two_le` * `polynomial.map_chebyshev₁` is now `polynomial.chebyshev.map_T` * `polynomial.chebyshev₂` is now `polynomial.chebyshev.U` * `polynomial.chebyshev₂_zero` is now `polynomial.chebyshev.U_zero` * `polynomial.chebyshev₂_one` is now `polynomial.chebyshev.U_one` * `polynomial.chebyshev₂_two` is now `polynomial.chebyshev.U_two` * `polynomial.chebyshev₂_add_two` is now `polynomial.chebyshev.U_add_two` * `polynomial.chebyshev₂_of_two_le` is now `polynomial.chebyshev.U_of_two_le` * `polynomial.chebyshev₂_eq_X_mul_chebyshev₂_add_chebyshev₁` is now `polynomial.chebyshev.U_eq_X_mul_U_add_T` * `polynomial.chebyshev₁_eq_chebyshev₂_sub_X_mul_chebyshev₂` is now `polynomial.chebyshev.T_eq_U_sub_X_mul_U` * `polynomial.chebyshev₁_eq_X_mul_chebyshev₁_sub_pol_chebyshev₂` is now `polynomial.chebyshev.T_eq_X_mul_T_sub_pol_U` * `polynomial.one_sub_X_pow_two_mul_chebyshev₂_eq_pol_in_chebyshev₁` is now `polynomial.chebyshev.one_sub_X_pow_two_mul_U_eq_pol_in_T` * `polynomial.map_chebyshev₂` is now `polynomial.chebyshev.map_U` * `polynomial.chebyshev₁_derivative_eq_chebyshev₂` is now `polynomial.chebyshev.T_derivative_eq_U` * `polynomial.one_sub_X_pow_two_mul_derivative_chebyshev₁_eq_poly_in_chebyshev₁` is now `polynomial.chebyshev.one_sub_X_pow_two_mul_derivative_T_eq_poly_in_T` * `polynomial.add_one_mul_chebyshev₁_eq_poly_in_chebyshev₂` is now `polynomial.chebyshev.add_one_mul_T_eq_poly_in_U` * `polynomial.mul_chebyshev₁` is now `polynomial.chebyshev.mul_T` * `polynomial.chebyshev₁_mul` is now `polynomial.chebyshev.T_mul` * `polynomial.dickson_one_one_eq_chebyshev₁` is now `polynomial.dickson_one_one_eq_chebyshev_T` * `polynomial.chebyshev₁_eq_dickson_one_one` is now `polynomial.chebyshev_T_eq_dickson_one_one` * `chebyshev₁_complex_cos` is now `polynomial.chebyshev.T_complex_cos` * `cos_nat_mul` is now `polynomial.chebyshev.cos_nat_mul` * `chebyshev₂_complex_cos` is now `polynomial.chebyshev.U_complex_cos` * `sin_nat_succ_mul` is now `polynomial.chebyshev.sin_nat_succ_mul` Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>