English
Evaluating at −2 gives (2) times n’s alternating power: (C_R(n)).eval(−2) = 2 · n.negOnePow.
Русский
Значение в −2 равно 2 · n.negOnePow: (C_R(n)).eval(−2) = 2 · (−1)^n.
LaTeX
$$$ (C_R(n)).eval(-2) = 2 \cdot n.negOnePow $$$
Lean4
@[simp]
theorem C_eval_neg_two (n : ℤ) : (C R n).eval (-2) = 2 * n.negOnePow := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1
ih2 =>
simp only [C_add_two, eval_sub, eval_mul, 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 [C_sub_one, eval_sub, eval_mul, 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
