aeval_subalgebra_coe

Mathlib.Algebra.Polynomial.AlgebraMap

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

← MathLib Explorer

English

For any polynomial p, the constant term equals the evaluation at 0: p(0) = aeval 0 p.

Русский

Для любого многочлена p постоянный член равен p(0) = aeval 0 p.

LaTeX

$$$p.c\text{oeff } 0 = \operatorname{aeval}(0) p.$$$

Lean4

@[norm_cast]
theorem aeval_subalgebra_coe (g : R[X]) {A : Type*} [Semiring A] [Algebra R A] (s : Subalgebra R A) (f : s) :
    (aeval f g : A) = aeval (f : A) g :=
  (aeval_algHom_apply s.val f g).symm

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

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

Разделы

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

Аффилиация

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