basis_empty

Mathlib.LinearAlgebra.Lagrange

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

English

If the index set is empty, the Lagrange basis polynomial corresponding to any node i is the constant polynomial 1.

Русский

Если множество индексов пусто, базис Лагранжа в любой узел i равен константному многочлену 1.

LaTeX

$$$L_{\emptyset,i}(X)=1$$$

Lean4

@[simp]
theorem basis_empty : Lagrange.basis ∅ v i = 1 :=
  rfl

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

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

Разделы

Аффилиация

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