isAlgClosed_of_perfectField — Mathlib

English

A separably closed perfect field is also algebraically closed.

Русский

Разделяемо замкнутое совершенное поле является алгебраически замкнутым.

LaTeX

$$$\text{IsSepClosed } k \land \text{PerfectField } k \Rightarrow \text{IsAlgClosed } k$$$

Lean4

/-- A separably closed perfect field is also algebraically closed. -/
instance (priority := 100) isAlgClosed_of_perfectField [IsSepClosed k] [PerfectField k] : IsAlgClosed k :=
  IsAlgClosed.of_exists_root k fun p _ h ↦
    exists_root p ((degree_pos_of_irreducible h).ne') (PerfectField.separable_of_irreducible h)

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