aeval_pi_apply₂

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.aeval_pi_apply₂

English

For any polynomial p, aeval X p = p.

Русский

Для любого многочлена p выполняется aeval X p = p.

LaTeX

$$$\forall p \in R[X],\; aeval X p = p.$$$

Lean4

theorem aeval_pi_apply₂ (j : I) : p.aeval x j = p.aeval (x j) :=
  aeval_pi (R := R) x ▸ Pi.algHom_apply R A (fun i ↦ aeval (x i)) p j

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

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

Разделы

Аффилиация

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