Commit 2021-03-06 01:08 44282437

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