Theorems · Definition · linear algebra

Lagrange.interpolate

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

Lagrange interpolation: given a finset s : Finset ι, a nodal map v : ι → F injective on s and a value function r : ι → F, interpolate s v r is the unique polynomial of degree < #s that takes value r i on v i for all i in s.

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

23 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq