eq_interpolate_of_eval_eq — Mathlib

English

The equivalence between (deg f < |s| and evaluations) and equality with interpolate.

Русский

Эквивалентность между (deg f < |s| и значениями) и равенством с interpolate.

LaTeX

$$(f.degree < #s ∧ ∀ i∈s, f(v i) = r i) ↔ f = interpolate s v r$$

Lean4

theorem eq_interpolate_of_eval_eq {f : F[X]} (hvs : Set.InjOn v s) (degree_f_lt : f.degree < #s)
    (eval_f : ∀ i ∈ s, f.eval (v i) = r i) : f = interpolate s v r :=
  by
  rw [eq_interpolate hvs degree_f_lt]
  exact interpolate_eq_of_values_eq_on _ _ eval_f

Похожие утверждения