English
The algebraic closure of F in E is the intermediate field consisting of all elements that are algebraic (equivalently integral) over F in E.
Русский
Алгебраическое замыкание F в E — это промежуточное поле, состоящее из всех элементов, являющихся алгебраическими (интегральными) над F в E.
LaTeX
$$$$\text{algebraicClosure } F E = \text{IntermediateField } F E \;\text{(consisting of algebraic elements)}$$$$
Lean4
/-- The *relative algebraic closure* of a field `F` in a field extension `E`,
also called the *maximal algebraic subextension* of `E / F`,
is defined to be the subalgebra `integralClosure F E`
upgraded to an intermediate field (since `F` and `E` are both fields).
This is exactly the intermediate field of `E / F` consisting of all integral/algebraic elements.
-/
@[stacks 09GI]
def algebraicClosure : IntermediateField F E :=
Algebra.IsAlgebraic.toIntermediateField (integralClosure F E)
