le_restrictScalars — Mathlib

English

If K/E/F is a tower, then algebraicClosure F K is contained in (algebraicClosure E K) restricted to F.

Русский

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

LaTeX

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

Lean4

/-- If `K / E / F` is a field extension tower, then `algebraicClosure F K` is contained in
`algebraicClosure E K`. -/
theorem le_restrictScalars [Algebra E K] [IsScalarTower F E K] :
    algebraicClosure F K ≤ (algebraicClosure E K).restrictScalars F := fun _ h ↦
  mem_algebraicClosure_iff.2 <| IsAlgebraic.tower_top E (mem_algebraicClosure_iff.1 h)

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