aeval_C

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

In the C-polynomials, aeval x (C_R n) = (C_R' n).eval x.

Русский

Для C-полиномов: aeval x (C_R n) = (C_R' n).eval x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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