basis_pair_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem basis_pair_left (hij : i ≠ j) : Lagrange.basis { i, j } v i = basisDivisor (v i) (v j) := by
  simp only [Lagrange.basis, hij, erase_insert_eq_erase, erase_eq_of_notMem, mem_singleton, not_false_iff,
    prod_singleton]

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