eq_zero_of_natDegree_lt_card_of_eval_eq_zero'

English

Let R be a domain and p ∈ R[x]. Let s be a finite set of scalars from R. If p(r) = 0 for all r ∈ s and natDegree(p) < card(s), then p = 0.

Русский

Пусть R — домен и p ∈ R[x]. Пусть s — конечный набор элементов из R. Если p(r) = 0 для всех r ∈ s и natDegree(p) < card(s), то p = 0.

LaTeX

$$$ p \in R[x],\; s \subseteq R,\; s \text{ finite},\; (\forall r \in s, \ p(r)=0),\; \operatorname{natDegree}(p) < |s| \Rightarrow p = 0.$$

Lean4

theorem eq_zero_of_natDegree_lt_card_of_eval_eq_zero' {R} [CommRing R] [IsDomain R] (p : R[X]) (s : Finset R)
    (heval : ∀ i ∈ s, p.eval i = 0) (hcard : natDegree p < #s) : p = 0 :=
  eq_zero_of_natDegree_lt_card_of_eval_eq_zero p Subtype.val_injective (fun i : s ↦ heval i i.prop)
    (hcard.trans_eq (Fintype.card_coe s).symm)

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