basis_pair_right

Mathlib.LinearAlgebra.Lagrange

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

← MathLib Explorer

English

For i ≠ j, the Lagrange basis on {i,j} at j equals basisDivisor(v_j, v_i).

Русский

Для i ≠ j базис Лагранжа на {i,j} в j равен basisDivisor(v_j, v_i).

LaTeX

$$$L_{\{i,j\},v,j}(X)=\operatorname{basisDivisor}(v_j,v_i)\quad (i\neq j)$$$

Lean4

@[simp]
theorem basis_pair_right (hij : i ≠ j) : Lagrange.basis { i, j } v j = basisDivisor (v j) (v i) :=
  by
  rw [pair_comm]
  exact basis_pair_left hij.symm

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

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

Разделы

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

Аффилиация

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