adjoin_le — Mathlib

English

If K/E/F is a tower, then the adjoin of algebraicClosure F K inside algebraicClosure E K is contained in algebraicClosure E K.

Русский

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

LaTeX

$$$ \\operatorname{adjoin}_E(\\operatorname{algebraicClosure}_F K) \\leq \\operatorname{algebraicClosure}_E K $$$

Lean4

/-- If `K / E / F` is a field extension tower, then `E` adjoin `algebraicClosure F K` is contained
in `algebraicClosure E K`. -/
theorem adjoin_le [Algebra E K] [IsScalarTower F E K] : adjoin E (algebraicClosure F K) ≤ algebraicClosure E K :=
  adjoin_le_iff.2 <| le_restrictScalars F E K

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