English
Let k be an algebraically closed field and R a semiring. If f : R →+* k is injective and p ∈ R[X] has nonzero degree, then p has a root in k after applying f to the coefficients; equivalently, there exists x ∈ k with p.eval₂ f x = 0.
Русский
Пусть k — алгебраически замкнутое поле и R — полупр. Если f : R →+* k инъективно и p ∈ R[X] не константный (deg p ≠ 0), то имеется корень x ∈ k such that p.eval₂ f x = 0.
LaTeX
$$$\forall \{R\} [\mathrm{Semiring\;R}] [\mathrm{IsAlgClosed\;k}] (f: R \to+* k) (hf: Function.Injective f) (p: R[x]) (hp: \deg p \neq 0), \exists x \in k, p.eval₂ f x = 0$$$
Lean4
theorem exists_eval₂_eq_zero_of_injective {R : Type*} [Semiring R] [IsAlgClosed k] (f : R →+* k)
(hf : Function.Injective f) (p : R[X]) (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0 :=
let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective hf])
⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩
