English
An intermediate field L ⊆ E is contained in algebraicClosure F E if all its elements are algebraic over F.
Русский
Пусть L — промежуточное поле в E. Тогда L ≤ algebraicClosure F E, если все элементы L алгебраичны над F.
LaTeX
$$$ L \\leq \\operatorname{algebraicClosure}_F(E) \\quad\\text{if } \\forall x\\in L,\\ IsAlgebraic}_F(x)$$$
Lean4
/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
if all of its elements are algebraic over `F`. -/
theorem le_algebraicClosure' {L : IntermediateField F E} (hs : ∀ x : L, IsAlgebraic F x) : L ≤ algebraicClosure F E :=
fun x h ↦ by
simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E, Algebra.algebraMap_self,
RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩
