English
For every integer n, (S_R(n)).eval(-2) = (-1)^n (n+1).
Русский
Для каждого целого n: (S_R(n)).eval(-2) = (-1)^n (n+1).
LaTeX
$$$ (S_R(n)).eval(-2) = (-1)^n \,(n+1) $$$
Lean4
@[simp]
theorem S_eval_neg_two (n : ℤ) : (S R n).eval (-2) = n.negOnePow * (n + 1) := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp; norm_num
| add_two n ih1
ih2 =>
simp only [S_add_two, eval_sub, eval_mul, eval_X, ih1, Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2,
Int.cast_ofNat, Int.negOnePow_add, Int.negOnePow_def 2]
norm_cast
norm_num
ring
| neg_add_one n ih1
ih2 =>
simp only [S_sub_one, eval_sub, eval_mul, eval_X, mul_neg, ih1, Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg,
neg_mul, ih2, Int.cast_add, Int.cast_one, Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]
norm_cast
norm_num
ring
