eq_zero_of_forall_eval_zero_of_natDegree_lt_card

English

If a polynomial f ∈ R[x] vanishes on every element of R and deg f < #R, then f = 0.

Русский

Если многочлен f ∈ R[x] обращается в нуль на каждом элементе множества R и deg f < |R|, то f = 0.

LaTeX

$$$ f \in R[x],\; \forall r \in R,\; f(r)=0,\; \operatorname{natDegree}(f) < |R| \Rightarrow f = 0.$$

Lean4

theorem eq_zero_of_forall_eval_zero_of_natDegree_lt_card (f : R[X]) (hf : ∀ r, f.eval r = 0) (hfR : f.natDegree < #R) :
    f = 0 := by
  obtain hR | hR := finite_or_infinite R
  · have := Fintype.ofFinite R
    apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero f Function.injective_id hf
    simpa only [mk_fintype, Nat.cast_lt] using hfR
  · exact zero_of_eval_zero _ hf

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