English
For an intermediate field L, L ≤ algebraicClosure F E if and only if L is algebraic over F.
Русский
Для промежуточного поля L верно: L ≤ algebraicClosure F E тогда и только если L алгебраично над F.
LaTeX
$$$ L \\leq \\operatorname{algebraicClosure}_F(E) \\iff \\operatorname{IsAlgebraic}_F(L) $$$
Lean4
/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
if and only if it is algebraic over `F`. -/
theorem le_algebraicClosure_iff (L : IntermediateField F E) : L ≤ algebraicClosure F E ↔ Algebra.IsAlgebraic F L :=
⟨fun h ↦
⟨fun x ↦ by
simpa only [IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E, IntermediateField.algebraMap_apply,
Algebra.algebraMap_self, RingHomCompTriple.comp_apply, mem_algebraicClosure_iff] using h x.2⟩,
fun _ ↦ le_algebraicClosure _ _ _⟩
