aeval_pi_apply

Mathlib.Algebra.Polynomial.AlgebraMap

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

← MathLib Explorer

English

The evaluation at X applied to p gives p itself.

Русский

Оценка в X для p возвращает сам p.

LaTeX

$$$((aeval X) p) = p$.$$

Lean4

/-- Polynomial evaluation on an indexed tuple is the indexed tuple of the evaluations
on the components.
Generalizes `Polynomial.aeval_prod_apply` to indexed products. -/
theorem aeval_pi_apply : p.aeval x = fun j ↦ p.aeval (x j) :=
  funext fun j ↦ aeval_pi_apply₂ x p j

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

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

Разделы

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

Аффилиация

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