English
For all integers n, (U_n)(-1) = (−1)^n (n+1).
Русский
Для любого целого n значение U_n(-1) равно (−1)^n (n+1).
LaTeX
$$$ (U(n))(-1) = (-1)^n \cdot (n+1) $$$
Lean4
@[simp]
theorem U_eval_neg_one (n : ℤ) : (U R n).eval (-1) = 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 [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, 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 [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, 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
