of_isAlgClosure_of_perfectField — Mathlib

English

If K is perfect and is an algebraic closure of k via an algebra structure, then it is also an algebraic closure of k and separable closure further

Русский

Если K совершенное поле и является алгебраическим замыканием k через структуру алгебры, то K является алгебраическим замыканием k (и сепарабельность сохраняется).

LaTeX

$$$IsAlgClosure k K$ and $IsSeparable k K$$$

Lean4

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

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