English
For algebraic E/F, separableClosure(F,E) = F if and only if E/F is purely inseparable.
Русский
Для алгебраического E/F сепарабельное замыкание F в E равно F тогда и только тогда, когда E/F чисто безразделимо.
LaTeX
$$$ separableClosure F E = ⊥ \iff IsPurelyInseparable F E $$$
Lean4
/-- If `E / F` is an algebraic extension, then the separable closure of `F` in `E` is
equal to `F` if and only if `E / F` is purely inseparable. -/
theorem eq_bot_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] :
separableClosure F E = ⊥ ↔ IsPurelyInseparable F E :=
⟨fun h ↦
isPurelyInseparable_iff.2 fun x ↦
⟨Algebra.IsIntegral.isIntegral x, fun hs ↦ by simpa only [h] using mem_separableClosure_iff.2 hs⟩,
fun _ ↦ eq_bot_of_isPurelyInseparable F E⟩
