aeval_coe_eq_smeval

Mathlib.Algebra.Polynomial.Smeval

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

← MathLib Explorer

English

The evaluation map at x coincides with smeval: for all p, aeval x p = p.smeval x.

Русский

Сопоставление aeval x совпадает с smeval: для любого p, aeval x p = p.smeval x.

LaTeX

$$∀ p, aeval\ x\ p = p.smeval\ x$$

Lean4

theorem aeval_coe_eq_smeval {R : Type*} [CommSemiring R] {S : Type*} [Semiring S] [Algebra R S] (x : S) :
    ⇑(aeval x) = fun (p : R[X]) => p.smeval x :=
  funext fun p => aeval_eq_smeval x p

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

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

Разделы

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

Аффилиация

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