basis — Mathlib

English

The basisDivisor has degree 1 when x ≠ y and degree 0 when x = y.

Русский

Базисный делитель имеет степень 1 при x ≠ y и 0 при x = y.

LaTeX

$$$$\\deg(\\mathrm{basisDivisor}(x,y)) = \\begin{cases}1,& x\\neq y,\\\\0,& x=y.\\end{cases}$$$$

Lean4

/-- Lagrange basis polynomials indexed by `s : Finset ι`, defined at nodes `v i` for a
map `v : ι → F`. For `i, j ∈ s`, `basis s v i` evaluates to 0 at `v j` for `i ≠ j`. When
`v` is injective on `s`, `basis s v i` evaluates to 1 at `v i`. -/
protected def basis (s : Finset ι) (v : ι → F) (i : ι) : F[X] :=
  ∏ j ∈ s.erase i, basisDivisor (v i) (v j)

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