evalEvalRingHom

Mathlib.Algebra.Polynomial.Bivariate

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

← MathLib Explorer

English

The evaluation-at-(x,y) map is a ring homomorphism from R[X][Y] to R.

Русский

Отображение оценки в (x,y) является кольцевым гомоморфизмом R[X][Y] → R.

LaTeX

$$$ evalEvalRingHom\\ (x)\\ (y) : R[X][Y] \\to\\+* R $$$

Lean4

/-- `evalEval x y` as a ring homomorphism. -/
@[simps!]
abbrev evalEvalRingHom (x y : R) : R[X][Y] →+* R :=
  (evalRingHom x).comp (evalRingHom <| C y)

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

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

Разделы

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

Аффилиация

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