eq_of_degrees_lt_of_eval_index_eq

English

If injOn v on s and deg f < |s| and f(v(i)) = g(v(i)) for all i ∈ s, 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 < |s|) \\Rightarrow (\\deg g < |s|) \\Rightarrow (\\forall i \\in s, f(v(i)) = g(v(i)) ) \\Rightarrow f=g.$$$$

Lean4

theorem eq_of_degrees_lt_of_eval_index_eq (hvs : Set.InjOn v s) (degree_f_lt : f.degree < #s)
    (degree_g_lt : g.degree < #s) (eval_fg : ∀ i ∈ s, f.eval (v i) = g.eval (v i)) : f = g :=
  by
  refine eq_of_degree_sub_lt_of_eval_index_eq _ hvs ?_ eval_fg
  rw [← mem_degreeLT] at degree_f_lt degree_g_lt ⊢
  exact Submodule.sub_mem _ degree_f_lt degree_g_lt

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