bump to nightly-2023-03-18-22

mathlib commit leanprover-community/mathlib@02ba894

Mathbin/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean

@@ -28,34 +28,34 @@ open Polynomial
 variable {R A : Type _} [CommRing R] [CommRing A] [Algebra R A]
 
 @[simp]
-theorem aeval_t (x : A) (n : ℕ) : aeval x (t R n) = (t A n).eval x := by
+theorem aeval_t (x : A) (n : ℕ) : aeval x (T R n) = (T A n).eval x := by
   rw [aeval_def, eval₂_eq_eval_map, map_T]
 #align polynomial.chebyshev.aeval_T Polynomial.Chebyshev.aeval_t
 
 @[simp]
-theorem aeval_u (x : A) (n : ℕ) : aeval x (u R n) = (u A n).eval x := by
+theorem aeval_u (x : A) (n : ℕ) : aeval x (U R n) = (U A n).eval x := by
   rw [aeval_def, eval₂_eq_eval_map, map_U]
 #align polynomial.chebyshev.aeval_U Polynomial.Chebyshev.aeval_u
 
 @[simp]
 theorem algebraMap_eval_t (x : R) (n : ℕ) :
-    algebraMap R A ((t R n).eval x) = (t A n).eval (algebraMap R A x) := by
+    algebraMap R A ((T R n).eval x) = (T A n).eval (algebraMap R A x) := by
   rw [← aeval_algebra_map_apply_eq_algebra_map_eval, aeval_T]
 #align polynomial.chebyshev.algebra_map_eval_T Polynomial.Chebyshev.algebraMap_eval_t
 
 @[simp]
 theorem algebraMap_eval_u (x : R) (n : ℕ) :
-    algebraMap R A ((u R n).eval x) = (u A n).eval (algebraMap R A x) := by
+    algebraMap R A ((U R n).eval x) = (U A n).eval (algebraMap R A x) := by
   rw [← aeval_algebra_map_apply_eq_algebra_map_eval, aeval_U]
 #align polynomial.chebyshev.algebra_map_eval_U Polynomial.Chebyshev.algebraMap_eval_u
 
 @[simp, norm_cast]
-theorem complex_of_real_eval_t : ∀ x n, ((t ℝ n).eval x : ℂ) = (t ℂ n).eval x :=
+theorem complex_of_real_eval_t : ∀ x n, ((T ℝ n).eval x : ℂ) = (T ℂ n).eval x :=
   @algebraMap_eval_t ℝ ℂ _ _ _
 #align polynomial.chebyshev.complex_of_real_eval_T Polynomial.Chebyshev.complex_of_real_eval_t
 
 @[simp, norm_cast]
-theorem complex_of_real_eval_u : ∀ x n, ((u ℝ n).eval x : ℂ) = (u ℂ n).eval x :=
+theorem complex_of_real_eval_u : ∀ x n, ((U ℝ n).eval x : ℂ) = (U ℂ n).eval x :=
   @algebraMap_eval_u ℝ ℂ _ _ _
 #align polynomial.chebyshev.complex_of_real_eval_U Polynomial.Chebyshev.complex_of_real_eval_u
 
@@ -71,7 +71,7 @@ variable (θ : ℂ)
 /-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
 value `cos (n * θ)`. -/
 @[simp]
-theorem t_complex_cos : ∀ n, (t ℂ n).eval (cos θ) = cos (n * θ)
+theorem t_complex_cos : ∀ n, (T ℂ n).eval (cos θ) = cos (n * θ)
   | 0 => by simp only [T_zero, eval_one, Nat.cast_zero, MulZeroClass.zero_mul, cos_zero]
   | 1 => by simp only [eval_X, one_mul, T_one, Nat.cast_one]
   | n + 2 =>
@@ -89,7 +89,7 @@ theorem t_complex_cos : ∀ n, (t ℂ n).eval (cos θ) = cos (n * θ)
 /-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
 value `sin ((n + 1) * θ) / sin θ`. -/
 @[simp]
-theorem u_complex_cos (n : ℕ) : (u ℂ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) :=
+theorem u_complex_cos (n : ℕ) : (U ℂ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) :=
   by
   induction' n with d hd
   · simp only [U_zero, Nat.cast_zero, eval_one, mul_one, zero_add, one_mul]
@@ -112,13 +112,13 @@ variable (θ : ℝ) (n : ℕ)
 /-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
 value `cos (n * θ)`. -/
 @[simp]
-theorem t_real_cos : (t ℝ n).eval (cos θ) = cos (n * θ) := by exact_mod_cast T_complex_cos θ n
+theorem t_real_cos : (T ℝ n).eval (cos θ) = cos (n * θ) := by exact_mod_cast T_complex_cos θ n
 #align polynomial.chebyshev.T_real_cos Polynomial.Chebyshev.t_real_cos
 
 /-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
 value `sin ((n + 1) * θ) / sin θ`. -/
 @[simp]
-theorem u_real_cos : (u ℝ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) := by
+theorem u_real_cos : (U ℝ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) := by
   exact_mod_cast U_complex_cos θ n
 #align polynomial.chebyshev.U_real_cos Polynomial.Chebyshev.u_real_cos