aevalTower_comp_toAlgHom

Mathlib.Algebra.Polynomial.AlgebraMap

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

← MathLib Explorer

English

Same content as the previous: aevalTower g y applied to toAlgHom of x equals g x.

Русский

То же самое: aevalTower g y от toAlgHom x даёт g x.

LaTeX

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

Lean4

@[simp]
theorem aevalTower_comp_toAlgHom : (aevalTower g y).comp (IsScalarTower.toAlgHom S R R[X]) = g :=
  AlgHom.coe_ringHom_injective <| aevalTower_comp_algebraMap _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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