le_algebraicClosure — Mathlib

English

If L is an intermediate field of E/F and L is algebraic over F, then L ≤ algebraicClosure F E.

Русский

Если L — промежуточное поле E/F и L алгебраично над F, то L содержится в algebraicClosure F E.

LaTeX

$$$ L \\leq \\operatorname{algebraicClosure}_F(E) \\quad\\text{if } \\text{IsAlgebraic}_F(L) $$$

Lean4

/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
if it is algebraic over `F`. -/
theorem le_algebraicClosure (L : IntermediateField F E) [Algebra.IsAlgebraic F L] : L ≤ algebraicClosure F E :=
  le_algebraicClosure' F E (Algebra.IsAlgebraic.isAlgebraic)

Похожие утверждения