nodalWeight_ne_zero

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

Each linear factor corresponding to a node divides the nodal polynomial.

Русский

Для i ∈ s, X − C(v(i)) делит nodal(s,v).

LaTeX

$$$ X - C(v(i)) \\mid nodal(s,v) $$$

Lean4

theorem nodalWeight_ne_zero (hvs : Set.InjOn v s) (hi : i ∈ s) : nodalWeight s v i ≠ 0 :=
  by
  rw [nodalWeight, prod_ne_zero_iff]
  intro j hj
  rcases mem_erase.mp hj with ⟨hij, hj⟩
  exact inv_ne_zero (sub_ne_zero_of_ne (mt (hvs.eq_iff hi hj).mp hij.symm))

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

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

Разделы

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

Аффилиация

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