aevalTower_toAlgHom

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

For x ∈ R, aevalTower g y (IsScalarTower.toAlgHom S R R[X] x) = g x, i.e., evaluating the algebra element x lands back at g.

Русский

Для x ∈ R верно: aevalTower g y (IsScalarTower.toAlgHom S R R[X] x) = g x.

LaTeX

$$aevalTower g y (IsScalarTower.toAlgHom S R R[X] x) = g x$$

Lean4

theorem aevalTower_toAlgHom (x : R) : aevalTower g y (IsScalarTower.toAlgHom S R R[X] x) = g x :=
  aevalTower_algebraMap _ _ _

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

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

Разделы

Аффилиация

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