English
Let R be a commutative semiring, k an algebraically closed field, and k an R-algebra. If the map algebraMap R k is injective, then for every p ∈ R[X] with deg p ≠ 0 there exists x ∈ k with aeval x p = 0.
Русский
Пусть R — коммутативный полугар, k — алгебраически замкнутое поле и k является R-алгеброй. Если algebraMap R k инъективна, то для любого p ∈ R[X] с deg p ≠ 0 существует x ∈ k такой, что aeval x p = 0.
LaTeX
$$$\forall \{R\} [\mathrm{CommSemiring\;R}] [\mathrm{IsAlgClosed\;k}] [\mathrm{Algebra\;R\;k}] (hinj: Function.Injective (algebraMap R k)) (p: R[x]) (hp: p.degree \neq 0), \exists x : k, aeval x p = 0$$$
Lean4
theorem exists_aeval_eq_zero_of_injective {R : Type*} [CommSemiring R] [IsAlgClosed k] [Algebra R k]
(hinj : Function.Injective (algebraMap R k)) (p : R[X]) (hp : p.degree ≠ 0) : ∃ x : k, aeval x p = 0 :=
exists_eval₂_eq_zero_of_injective (algebraMap R k) hinj p hp
