coe_aeval_eq_eval

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

For any φ : R[X] →ₐ[R] A, φ(p) = eval₂(algebraMap R A, φ X) p.

Русский

Для любого φ: R[X] →ₐ[R] A выполняется φ(p) = eval₂(algebraMap R A, φ X) p.

LaTeX

$$$\forall \phi: R[X] \rightarrow_{R} A,\; \phi(p) = \operatorname{eval}_2(\operatorname{algebraMap} R A, \phi X) p.$$$

Lean4

@[simp]
theorem coe_aeval_eq_eval (r : R) : (aeval r : R[X] → R) = eval r :=
  rfl

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

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

Разделы

Аффилиация

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