exists_root — Mathlib

English

Let k be a separably closed field. If p ∈ k[X] has nonzero degree and is separable, then p has a root in k.

Русский

Пусть k — сепарабельное замкнутое поле. Если p ∈ k[X] ненулевая, и p сепарабельен, то p имеет корень в k.

LaTeX

$$$p.d e g r e e \neq 0 \wedge p.Separable \Rightarrow \exists x\, p.IsRoot x$$$

Lean4

theorem exists_root [IsSepClosed k] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x, IsRoot p x :=
  exists_root_of_splits _ (IsSepClosed.splits_of_separable p hsep) hp

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