aeval_S

Mathlib.RingTheory.Polynomial.Chebyshev

URI: https://scilib.ai/kg/mathlib#Polynomial.Chebyshev.aeval_S

English

For all x and n, aeval x (S_R n) = (S_R' n).eval x.

Русский

Для всех x и n: aeval x (S_R n) = (S_R' n).eval x.

LaTeX

$$$ aeval\ x\ (S_R\ n) = (S_R'\ n).eval\ x $$$

Lean4

@[simp]
theorem aeval_S [Algebra R R'] (x : R') (n : ℤ) : aeval x (S R n) = (S R' n).eval x := by
  rw [aeval_def, eval₂_eq_eval_map, map_S]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru