eq_restrictScalars_of_isAlgebraic

English

If E/F is algebraic, then algebraicClosure F K equals the restriction to F of algebraicClosure E K.

Русский

Если E/F алгебраично, то algebraicClosure F K равняется ограничению по F от algebraicClosure E K.

LaTeX

$$$ \\operatorname{algebraicClosure}_F(K) = (\\operatorname{algebraicClosure}_E(K))_{|F} $$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then
`algebraicClosure F K` is equal to `algebraicClosure E K`. -/
theorem eq_restrictScalars_of_isAlgebraic [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] :
    algebraicClosure F K = (algebraicClosure E K).restrictScalars F :=
  (algebraicClosure.le_restrictScalars F E K).antisymm fun _ h ↦ isIntegral_trans _ h

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