isSepClosed — Mathlib

English

If E/F is algebraic and F is separably closed, then E is separably closed.

Русский

Если E/F алгебраично, и F сепарабельное, тогда E сепарабельное.

LaTeX

$$$\text{IsSepClosed } E$$$

Lean4

/-- If `E / F` is an algebraic extension, `F` is separably closed,
then `E` is also separably closed. -/
theorem isSepClosed [Algebra.IsAlgebraic F E] [IsSepClosed F] : IsSepClosed E :=
  have : Algebra.IsAlgebraic F (AlgebraicClosure E) := .trans F E _
  (isSepClosed_iff_isPurelyInseparable_algebraicClosure E _).mpr
    (IsPurelyInseparable.tower_top F E <| AlgebraicClosure E)

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