Theorems · Theorem · linear algebra

Lagrange.eq_interpolate_iff

∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
  {f : Polynomial F},
  Set.InjOn v ↑s → ((f.degree < ↑s.card ∧ ∀ i ∈ s, Polynomial.eval (v i) f = r i) ↔ f = (Lagrange.interpolate s v) r)

This is the characteristic property of the interpolation: the interpolation is the unique polynomial of degree < Fintype.card ι which takes the value of the r i on the v i.

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq