nodal_insert_eq_nodal

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

Adding a new node multiplies the nodal polynomial by the corresponding linear factor.

Русский

Если i не в s, то nodal(insert i s) v = (X − C(v(i))) · nodal s v.

LaTeX

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

Lean4

theorem nodal_insert_eq_nodal [DecidableEq ι] {i : ι} (hi : i ∉ s) : nodal (insert i s) v = (X - C (v i)) * nodal s v :=
  by simp_rw [nodal, prod_insert hi]

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

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

Разделы

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

Аффилиация

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