English
Let R be a commutative domain and p be a polynomial in R[x]. If I is a finite index set and f : I → R is injective, and p(f(i)) = 0 for every i ∈ I, while natDegree(p) < |I|, then p = 0.
Русский
Пусть R — коммутативное кольцо без нулевых делителей и p ∈ R[x]. Пусть I — конечное множество индексов и f: I → R инъективно, причём p(f(i)) = 0 для всех i ∈ I, и natDegree(p) < |I|. Тогда p = 0.
LaTeX
$$$ p \in R[x],\; \iota \text{ — конечное множество},\; f: \iota \to R \text{ инъекция},\; p(f(i)) = 0 \text{ для всех } i \in \iota,\; \operatorname{natDegree}(p) < |\iota| \Longrightarrow p = 0.$$
Lean4
theorem eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R] (p : R[X]) {ι} [Fintype ι]
{f : ι → R} (hf : Function.Injective f) (heval : ∀ i, p.eval (f i) = 0) (hcard : natDegree p < Fintype.card ι) :
p = 0 := by
classical
by_contra hp
refine lt_irrefl (#p.roots.toFinset) ?_
calc
#p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
_ ≤ natDegree p := (Polynomial.card_roots' p)
_ < Fintype.card ι := hcard
_ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
_ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
_ ≤ #p.roots.toFinset := Finset.card_mono ?_
intro _
simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq, IsRoot.def,
forall_exists_index, hp, not_false_eq_true]
rintro x rfl
exact heval _
