S_comp_two_mul_X — Mathlib

English

For every integer n, the composition of S_R(n) with the polynomial 2X equals U_R(n): (S_R(n)).comp(2 X) = U_R(n).

Русский

Для каждого целого n: композиция S_R(n) с 2X дает U_R(n): (S_R(n)).comp(2 X) = U_R(n).

LaTeX

$$$ (S_R(n)).\circ(2 X) = U_R(n) $$$

Lean4

theorem S_comp_two_mul_X (n : ℤ) : (S R n).comp (2 * X) = U R n := by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

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