English
An intermediate field L equals separableClosure F E iff it is separable over F and E is purely inseparable over L.
Русский
Промежуточное поле L равно separableClosure(F,E) тогда и только тогда, когда оно сепарабельно над F и E чисто бесприводно над L.
LaTeX
$$$L = \mathrm{separableClosure} F E \iff (\mathrm Algebra.IsSeparable F L) \wedge (\mathrm IsPurelyInseparable L E)$$$
Lean4
/-- If an intermediate field of `E / F` is separable over `F`, and `E` is purely inseparable
over it, then it is equal to the separable closure of `F` in `E`. -/
theorem eq_separableClosure (L : IntermediateField F E) [Algebra.IsSeparable F L] [IsPurelyInseparable L E] :
L = separableClosure F E :=
le_antisymm (le_separableClosure F E L) (separableClosure_le F E L)
