English
Let R be a commutative ring. For every integer n, the evaluation at -1 of the nth Chebyshev polynomial of the first kind equals (-1)^n.
Русский
Пусть R — коммутативное кольцо. Для каждого целого числа n значение n-йChebyshev-полиномы первого рода в точке −1 равно (−1)^n.
LaTeX
$$$ (T_R(n))(-1) = (-1)^n \quad \text{for all } n \in \mathbb{Z}. $$$
Lean4
@[simp]
theorem T_eval_neg_one (n : ℤ) : (T R n).eval (-1) = n.negOnePow := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1
ih2 =>
simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, Int.negOnePow_add,
Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2, Int.negOnePow_def 2]
norm_cast
norm_num
ring
| neg_add_one n ih1
ih2 =>
simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul, ih2,
Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add, Int.negOnePow_sub]
ring
