exists_root — Mathlib

English

If k is algebraically closed and p ∈ k[X] is nonconstant, then p has a root in k.

Русский

Если k алгебраически замкнутое и p ненулевой, тогда p имеет корень в k.

LaTeX

$$$\exists x\in k, \ p(x)=0$ for nonconstant p.$$

Lean4

/-- If `k` is algebraically closed, then every nonconstant polynomial has a root.
-/
@[stacks 09GR "(4) ⟹ (3)"]
theorem exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x :=
  exists_root_of_splits _ (IsAlgClosed.splits p) hp

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