exists_eval₂_eq_zero — Mathlib

English

Let R be a division ring and k an algebraically closed field. For any f : R →+* k and polynomial p ∈ R[X] with deg p ≠ 0 there exists x ∈ k such that p.eval₂ f x = 0.

Русский

Пусть R — деление кольца, k — алгебраически замкнутое поле. Для любого f : R →+* k и p ∈ R[X] с deg p ≠ 0 существует x ∈ k such that p.eval₂ f x = 0.

LaTeX

$$$\forall \{R\} [\mathrm{DivisionRing\;R}] [\mathrm{IsAlgClosed\;k}] (f: R \to+* k) (p: R[x]) (hp: p.degree \neq 0), \exists x, p.eval₂ f x = 0$$$

Lean4

theorem exists_eval₂_eq_zero {R : Type*} [DivisionRing R] [IsAlgClosed k] (f : R →+* k) (p : R[X]) (hp : p.degree ≠ 0) :
    ∃ x, p.eval₂ f x = 0 :=
  exists_eval₂_eq_zero_of_injective f f.injective p hp

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