S_eval_two — Mathlib

English

For every integer n, the evaluation of S_R(n) at 2 equals n+1: (S_R(n)).eval(2) = n+1.

Русский

Для каждого целого n значение S_R(n) в точке 2 равно n+1: (S_R(n)).eval(2) = n+1.

LaTeX

$$$ (S_R(n)).eval(2) = n + 1 $$$

Lean4

@[simp]
theorem S_eval_two (n : ℤ) : (S R n).eval 2 = 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, ih2,
      Int.cast_ofNat]
    ring
  | neg_add_one n ih1
    ih2 =>
    simp only [S_sub_one, eval_sub, eval_mul, eval_X, ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add,
      Int.cast_one, Int.cast_sub, sub_add_cancel]
    ring

Похожие утверждения