nodal_erase_eq_nodal_div

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

All nodal weights are nonzero for i in s.

Русский

Для i ∈ s вес nodalWeight(s,v,i) не равен нулю.

LaTeX

$$$ \\operatorname{nodalWeight}(s,v,i) \\neq 0. $$$

Lean4

theorem nodal_erase_eq_nodal_div (hi : i ∈ s) : nodal (s.erase i) v = nodal s v / (X - C (v i)) :=
  by
  rw [nodal_eq_mul_nodal_erase hi, mul_div_cancel_left₀]
  exact X_sub_C_ne_zero _

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

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

Разделы

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

Аффилиация

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