eval₂Hom_zero_apply

Mathlib.Algebra.MvPolynomial.Eval

URI: https://scilib.ai/kg/mathlib#MvPolynomial.eval₂Hom_zero_apply

← MathLib Explorer

English

For any polynomial p, eval₂Hom f (0) p equals f(constantCoeff p).

Русский

Для любого многочлена p, eval₂Hom f(0) p равно f(constantCoeff(p)).

LaTeX

$$$$ \mathrm{eval_2Hom\,zero\,apply}(f,p) = f( \text{constantCoeff}(p) ) $$$$

Lean4

theorem eval₂Hom_zero_apply (f : R →+* S₂) (p : MvPolynomial σ R) : eval₂Hom f (0 : σ → S₂) p = f (constantCoeff p) :=
  RingHom.congr_fun (eval₂Hom_zero f) p

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

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

Разделы

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

Аффилиация

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