basis_singleton

Mathlib.LinearAlgebra.Lagrange

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

English

If the index set is a singleton {i}, the Lagrange basis at i is the constant polynomial 1.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem basis_singleton (i : ι) : Lagrange.basis { i } v i = 1 := by rw [Lagrange.basis, erase_singleton, prod_empty]

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

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

Разделы

Аффилиация

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