isSepClosed_iff_isPurelyInseparable_algebraicClosure

English

If E is an algebraic closure of F, then F is separably closed iff E/F is purely inseparable.

Русский

Если E — алгебраическое замыкание F, тогда F сепарабельное тогда и только тогда, когда E/F чисто бесприводно.

LaTeX

$$$\text{IsSepClosed } F \iff \text{IsPurelyInseparable } F E$$$

Lean4

/-- If `E` is an algebraic closure of `F`, then `F` is separably closed if and only if `E / F` is
purely inseparable. -/
theorem isSepClosed_iff_isPurelyInseparable_algebraicClosure [IsAlgClosure F E] :
    IsSepClosed F ↔ IsPurelyInseparable F E :=
  ⟨fun _ ↦ inferInstance, fun H ↦ by
    haveI := IsAlgClosure.isAlgClosed F (K := E)
    rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H⟩

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