English
Equality from degree bound and evaluation on a finite set: if injOn v on s and deg f ≤ |s| and f(v(i)) = g(v(i)) for all i ∈ s, with leading coefficients matching, then f = g.
Русский
Если injOn v на s и deg f ≤ |s| и f(v(i)) = g(v(i)) для всех i ∈ s, и ведущие коэффициенты совпадают, то f = g.
LaTeX
$$$$\\mathrm{injOn}(v,s) \\Rightarrow (\\deg f \\le |s|) \\Rightarrow (\\deg f = \\deg g) \\Rightarrow (\\forall i \\in s, f(v(i)) = g(v(i))) \\Rightarrow f=g.$$$$
Lean4
/-- `basisDivisor x y` is the unique linear or constant polynomial such that
when evaluated at `x` it gives `1` and `y` it gives `0` (where when `x = y` it is identically `0`).
Such polynomials are the building blocks for the Lagrange interpolants. -/
def basisDivisor (x y : F) : F[X] :=
C (x - y)⁻¹ * (X - C y)
