nodal_eq

Mathlib.LinearAlgebra.Lagrange

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

English

As above, the nodal polynomial is the product of linear factors corresponding to the nodes.

Русский

nodal(s,v) равно произведению ∏_{i∈s} (X − C(v(i))).

LaTeX

$$$ \\operatorname{nodal}(s,v) = \\prod_{i\\in s} (X - C(v(i))). $$$

Lean4

theorem nodal_eq (s : Finset ι) (v : ι → R) : nodal s v = ∏ i ∈ s, (X - C (v i)) :=
  rfl

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

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

Разделы

Аффилиация

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