eq_zero_of_degree_lt_of_eval_finset_eq_zero

English

If deg f < |s| and f vanishes on s, then f is the zero polynomial.

Русский

Если deg f < |s| и f обнуляется на каждом элементе s, то f равно нулю.

LaTeX

$$$$\\deg f < |s| \\quad\\text{and}\\quad (\\forall x\\in s)\\; f(x)=0 \\quad\\Rightarrow\\quad f=0.$$$$

Lean4

theorem eq_zero_of_degree_lt_of_eval_finset_eq_zero (degree_f_lt : f.degree < #s) (eval_f : ∀ x ∈ s, f.eval x = 0) :
    f = 0 := by
  rw [← mem_degreeLT] at degree_f_lt
  simp_rw [eval_eq_sum_degreeLTEquiv degree_f_lt] at eval_f
  rw [← degreeLTEquiv_eq_zero_iff_eq_zero degree_f_lt]
  exact
    Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero
      (Injective.comp (Embedding.subtype _).inj' (equivFinOfCardEq (card_coe _)).symm.injective) fun _ =>
      eval_f _ (Finset.coe_mem _)

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