fieldRange_le_normalClosure — Mathlib

English

If K/F is algebraic, then the normal closure is contained in the iSup of the adjoined root sets of the minPolys of elements of K in L.

Русский

Если K/F алгебраическое, нормальное замыкание ⊆ iSup(adjoin rootSet(minpoly(x))) для x∈K в L.

LaTeX

$$$\normalClosure(F,K,L) \le \big\langle x:\,K \mapsto adjoin(F\, (\minpoly(F,x).rootSet\;L))\big\rangle$$$

Lean4

theorem fieldRange_le_normalClosure (f : K →ₐ[F] L) : f.fieldRange ≤ normalClosure F K L :=
  le_iSup AlgHom.fieldRange f

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