eq_of_degrees_lt_of_eval_finset_eq

English

If f and g have degrees less than |s| and agree on s, then f = g.

Русский

Если степени f и g меньше |s| и они совпадают на s, то f = g.

LaTeX

$$$$\\deg f < |s| \\quad\\wedge\\quad \\deg g < |s| \\quad\\wedge\\quad (\\forall x\\in s),\\; f(x)=g(x) \\Rightarrow f=g.$$$$

Lean4

theorem eq_of_degrees_lt_of_eval_finset_eq (degree_f_lt : f.degree < #s) (degree_g_lt : g.degree < #s)
    (eval_fg : ∀ x ∈ s, f.eval x = g.eval x) : f = g :=
  by
  rw [← mem_degreeLT] at degree_f_lt degree_g_lt
  refine eq_of_degree_sub_lt_of_eval_finset_eq _ ?_ eval_fg
  rw [← mem_degreeLT]; exact Submodule.sub_mem _ degree_f_lt degree_g_lt

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