T_eval_one — Mathlib

English

For integer n, the value of T evaluated at 1 equals 1: (T R n).eval 1 = 1.

Русский

Для любого целого n значение T, вычисленное в 1, равно 1.

LaTeX

$$$(T\\,R\\, n).eval(1) = 1$$$

Lean4

@[simp]
theorem T_eval_one (n : ℤ) : (T R n).eval 1 = 1 := by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num

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