English
If E/F is algebraic and L is separable over F with E purely inseparable over L, then L equals separableClosure F E.
Русский
Если E/F алгебраично и L сепарабельно над F, а E чисто бесприводно над L, то L = separableClosure F E.
LaTeX
$$$L = \mathrm{separableClosure} F E$$$
Lean4
/-- If `E / F` is algebraic, then an intermediate field of `E / F` is equal to the separable closure
of `F` in `E` if and only if it is separable over `F`, and `E` is purely inseparable
over it. -/
theorem eq_separableClosure_iff [Algebra.IsAlgebraic F E] (L : IntermediateField F E) :
L = separableClosure F E ↔ Algebra.IsSeparable F L ∧ IsPurelyInseparable L E :=
⟨by rintro rfl; exact ⟨isSeparable F E, isPurelyInseparable F E⟩, fun ⟨_, _⟩ ↦ eq_separableClosure F E L⟩
