isAlgClosure_of_perfectField_top — Mathlib

English

In a separably closed k, for any x and natural n, there exists z with z^n = x (when n nonzero in k).

Русский

В сепарабельном замкнутом поле существует n-ый корень любого элемента при n != 0 в поле.

LaTeX

$$∃ z: z^n = x$$

Lean4

/-- If `K` is perfect and is a separable closure of `k`,
then it is also an algebraic closure of `k`. -/
instance (priority := 100) isAlgClosure_of_perfectField_top [Algebra k K] [IsSepClosure k K] [PerfectField K] :
    IsAlgClosure k K :=
  haveI : IsSepClosed K := IsSepClosure.sep_closed k
  ⟨inferInstance, IsSepClosure.separable.isAlgebraic⟩

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