exists_aeval_eq_zero — Mathlib

English

Let R be a field and k an algebraically closed field with an R-algebra structure. For any p ∈ R[X] with deg p ≠ 0 there exists x ∈ k such that aeval x p = 0.

Русский

Пусть R — поле и k — алгебраически замкнутое поле с структурой R-алгебры. Для любого p ∈ R[X] с deg p ≠ 0 существует x ∈ k такой, что aeval x p = 0.

LaTeX

$$$\forall (R) [\mathrm{Field\;R}] [\mathrm{IsAlgClosed\;k}] [\mathrm{Algebra\;R\;k}] (p: R[X]), p.degree \neq 0 \to \exists x \in k, aeval x p = 0$$$

Lean4

theorem exists_aeval_eq_zero {R : Type*} [Field R] [IsAlgClosed k] [Algebra R k] (p : R[X]) (hp : p.degree ≠ 0) :
    ∃ x : k, aeval x p = 0 :=
  exists_eval₂_eq_zero (algebraMap R k) p hp

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