aevalTower_algebraMap

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.aevalTower_algebraMap

English

Composing aevalTower with the canonical algebra map R → Polynomial R[X] yields g: (aevalTower g y) ∘ (algebraMap R (Polynomial R)) = g.

Русский

Составление aevalTower с каноническим отображением алгебры R → Polynomial R[X] даёт g.

LaTeX

$$(aevalTower g y) ∘ (algebraMap R (Polynomial R)) = g$$

Lean4

theorem aevalTower_algebraMap (x : R) : aevalTower g y (algebraMap R R[X] x) = g x :=
  eval₂_C _ _

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

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

Разделы

Аффилиация

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