eval_nodal_at_node

Mathlib.LinearAlgebra.Lagrange

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

English

Each node is a root of the nodal polynomial.

Русский

Если i ∈ s, то f(v(i)) = 0; eval_{v(i)} nodal(s,v) = 0.

LaTeX

$$$ \\operatorname{eval}(\\,v(i)\,)(\\operatorname{nodal}(s,v)) = 0 \\quad\\text{for } i\\in s. $$$

Lean4

theorem eval_nodal_at_node {i : ι} (hi : i ∈ s) : eval (v i) (nodal s v) = 0 :=
  by
  rw [eval_nodal]
  exact s.prod_eq_zero hi (sub_self (v i))

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

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

Разделы

Аффилиация

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