eq_zero_of_degree_lt_of_eval_index_eq_zero

English

If injOn v on s and deg f < |s| with f(v(i)) = 0 for all i ∈ s, then f = 0.

Русский

Если отображение v инъективно на s и deg f < |s|, а f(v(i)) = 0 для всех i ∈ s, то f = 0.

LaTeX

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

Lean4

theorem eq_zero_of_degree_lt_of_eval_index_eq_zero (hvs : Set.InjOn v s) (degree_f_lt : f.degree < #s)
    (eval_f : ∀ i ∈ s, f.eval (v i) = 0) : f = 0 := by
  classical
  rw [← card_image_of_injOn hvs] at degree_f_lt
  refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
  intro x hx
  rcases mem_image.mp hx with ⟨_, hj, rfl⟩
  exact eval_f _ hj

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