U_eval_one — Mathlib

English

For every integer n, the value of U_n at 1 is n+1.

Русский

Для каждого целого n значение U_n в точке 1 равно n+1.

LaTeX

$$$ (U(n))\!\text{(at } 1) = n+1 $$$

Lean4

@[simp]
theorem U_eval_one (n : ℤ) : (U R n).eval 1 = 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_one, ih1, Int.cast_add, Int.cast_natCast,
      Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1
    ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1, Int.cast_neg, Int.cast_natCast, ih2,
      Int.cast_add, Int.cast_one, Int.cast_sub, sub_add_cancel]
    ring

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