Theorems · Definition · linear algebra

Lagrange.basis

{F : Type u_1} → [inst : Field F] → {ι : Type u_2} → [DecidableEq ι] → Finset ι → (ι → F) → ι → Polynomial F

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.

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

26 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDecidableEq