English
The separable closure is algebraic over the base field.
Русский
Разделимое замыкание является алгебраическим над базовым полем.
LaTeX
$$$\\text{IsAlgebraic } F (\\text{separableClosure } F E)$$$
Lean4
/-- The (relative) separable closure of `F` in `E`, or called maximal separable subextension
of `E / F`, is defined to be the intermediate field of `E / F` consisting of all separable
elements. The previous results prove that these elements are closed under field operations. -/
@[stacks 09HC]
def separableClosure : IntermediateField F E
where
carrier := {x | IsSeparable F x}
mul_mem' := isSeparable_mul
add_mem' := isSeparable_add
algebraMap_mem' := isSeparable_algebraMap E
inv_mem' _ := isSeparable_inv
