English
The SeparableClosure object is defined as the separable closure inside the algebraic closure.
Русский
Объект SeparableClosure определяется как разделимое замыкание внутри алгебраического замыкания.
LaTeX
$$abbrev SeparableClosure := separableClosure F (AlgebraicClosure F)$$
Lean4
/-- The absolute separable closure is defined to be the relative separable closure inside the
algebraic closure. It is indeed a separable closure (`IsSepClosure`) by
`separableClosure.isSepClosure`, and it is Galois (`IsGalois`) by `separableClosure.isGalois`
or `IsSepClosure.isGalois`, and every separable extension embeds into it (`IsSepClosed.lift`). -/
abbrev SeparableClosure : Type _ :=
separableClosure F (AlgebraicClosure F)
