A well known result from algebra is that, on any field, there
is exactly one polynomial of degree less than n interpolating n points
[1,
§7]. This entry contains a formalization of the
above result, as well as the following generalization in the case of
finite fields *F*: There are
*|F|*^{m-n} polynomials of degree
less than *m ≥ n* interpolating the same n points,
where *|F|* denotes the size of the domain of the
field. To establish the result the entry also includes a formalization
of Lagrange interpolation, which might be of independent
interest. The formalized results are defined on the
algebraic structures from HOL-Algebra, which are distinct from the
type-class based structures defined in HOL. Note that there is an
existing formalization for polynomial interpolation and, in
particular, Lagrange interpolation by Thiemann and Yamada [2]
on the type-class based structures in HOL. |