aeval_T

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

For any R, R' with R-algebra, and x in R', aeval x (T_R n) = (T_R' n).eval x.

Русский

При любых кольцах R, R' с алгеброй над R и x ∈ R', выполняется aeval x (T_R n) = (T_R' n).eval x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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