eq_of_degree_sub_lt_of_eval_index_eq

English

Equality by subtraction with index: if deg(f−g) < |s| and f(v(i)) = g(v(i)) for all i ∈ s, then f = g.

Русский

Если deg(f−g) < |s| и f(v(i)) = g(v(i)) для всех i ∈ s, то f = g.

LaTeX

$$$$\\deg(f-g) < |s| \\land (\\forall i \\in s),\\; f(v(i)) = g(v(i)) \\Rightarrow f=g.$$$$

Lean4

theorem eq_of_degree_sub_lt_of_eval_index_eq (hvs : Set.InjOn v s) (degree_fg_lt : (f - g).degree < #s)
    (eval_fg : ∀ i ∈ s, f.eval (v i) = g.eval (v i)) : f = g :=
  by
  rw [← sub_eq_zero]
  refine eq_zero_of_degree_lt_of_eval_index_eq_zero _ hvs degree_fg_lt ?_
  simp_rw [eval_sub, sub_eq_zero]
  exact eval_fg

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