eval₂_X_mul

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

Yet another form of the list-sum evaluation property.

Русский

Ещё одно выражение свойства суммы по списку.

LaTeX

$$$\operatorname{ev}_{f,x}\bigl(\text{List}.sum l\bigr) = \sum_{p \in l} \operatorname{ev}_{f,x}(p)$$$

Lean4

@[simp]
theorem eval₂_X_mul : eval₂ f x (X * p) = eval₂ f x p * x := by rw [X_mul, eval₂_mul_X]

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

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

Разделы

Аффилиация

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