English
The Chebyshev polynomials satisfy T(-n) = T(n) for all integers n; i.e., they are even functions in the integer index.
Русский
Чебышёвские полиномы удовлетворяют T(−n) = T(n) для всех целых n; они чётны относительно индекса.
LaTeX
$$T_R(-n) = T_R(n)$$
Lean4
@[simp]
theorem T_neg (n : ℤ) : T R (-n) = T R n := by
induction n using Polynomial.Chebyshev.induct with
| zero => rfl
| one => simp only [T_neg_one, T_one]
| add_two n ih1 ih2 =>
have h₁ := T_add_two R n
have h₂ := T_sub_two R (-n)
linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
| neg_add_one n ih1 ih2 =>
have h₁ := T_add_one R n
have h₂ := T_sub_one R (-n)
linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂
