normalClosure_eq_iSup_adjoin — Mathlib

English

If K/F is algebraic, IsNormalClosure F K L is equivalent to the conjunction of the splits condition for all x in K and the normal closure being top.

Русский

Если K/F алгебраическое, то IsNormalClosure F K L эквивалентно сочетанию условия распада для каждого x в K и того, что нормальное замыкание равно топу.

LaTeX

$$$IsNormalClosure\ F\ K\ L \iff \Big(\forall x:K, (minpoly F x).Splits (algebraMap F L)\Big) \land normalClosure F K L = \top$$$

Lean4

theorem normalClosure_eq_iSup_adjoin [Algebra K L] [IsScalarTower F K L] [Normal F L] :
    normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L) :=
  normalClosure_eq_iSup_adjoin' (ne := ⟨IsScalarTower.toAlgHom F K L⟩)

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