eval_nodal

Mathlib.LinearAlgebra.Lagrange

URI: https://scilib.ai/kg/mathlib#Lagrange.eval_nodal

English

The evaluation of nodal is given by the pointwise product of (x − v(i)).

Русский

Значение nodal(s,v) в x равно произведению над i∈s: (x − v(i)).

LaTeX

$$$ \\operatorname{eval}_x (\\operatorname{nodal}(s,v)) = \\prod_{i\\in s} (x - v(i)). $$$

Lean4

theorem eval_nodal {x : R} : (nodal s v).eval x = ∏ i ∈ s, (x - v i) := by
  simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]

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

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

Разделы

Аффилиация

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