Theorems · Definition · linear algebra

Lagrange.nodal

{R : Type u_1} → [inst : CommRing R] → {ι : Type u_2} → Finset ι → (ι → R) → Polynomial R

nodal s v is the unique monic polynomial whose roots are the nodes defined by v and s. That is, the roots of nodal s v are exactly the image of v on s, with appropriate multiplicity. We can use nodal to define the barycentric forms of the evaluated interpolant.

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

24 results in Mathlib

Foundations

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

Assumes

CommRing