Update Mathlib/RingTheory/Polynomial/Chebyshev.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: YuvalFilmus

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -490,7 +490,7 @@ theorem T_eq_X_mul_U_sub_U (n : ℤ) : T R (n + 2) = X * U R (n + 1) - U R n :=
     show n + 2 + 1 - 2 = n + 1 by ring] at h
   linear_combination (norm := ring_nf) h
 
-theorem twice_T_eq_U_sub_U (n : ℤ) : 2 * T R (n + 2) = U R (n + 2) - U R n := by
+theorem two_mul_T_eq_U_sub_U (n : ℤ) : 2 * T R (n + 2) = U R (n + 2) - U R n := by
   linear_combination (norm := ring_nf) (T_eq_U_sub_X_mul_U R (n + 2)) + (T_eq_X_mul_U_sub_U R n)
 
 theorem U_eq_twice_T_add_U (n : ℤ) : U R (n + 2) = 2 * T R (n + 2) + U R n := by