exists_eval_ne_zero_of_natDegree_lt_card

English

For a nonzero polynomial f ∈ R[x] over a domain R with deg f < #R, there exists r ∈ R such that f(r) ≠ 0 after applying an injective map to another domain.

Русский

Для не нулевого многочлена f ∈ R[x] над доменом R с deg f < #R существует r ∈ R с f(r) ≠ 0 после отображения в другое домену.

LaTeX

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

Lean4

theorem exists_eval_ne_zero_of_natDegree_lt_card (f : R[X]) (hf : f ≠ 0) (hfR : f.natDegree < #R) : ∃ r, f.eval r ≠ 0 :=
  by
  contrapose! hf
  exact eq_zero_of_forall_eval_zero_of_natDegree_lt_card f hf hfR

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