normal — Mathlib

English

A normal closure is always a normal extension. If IsNormalClosure F K L holds, then L is a normal extension of F.

Русский

Нормальное замыкание всегда нормальное расширение. Если IsNormalClosure F K L выполняется, то L является нормальным расширением над F.

LaTeX

$$$\text{IsNormalClosure}(F,K,L)\Rightarrow \text{Normal}(F,L)$$$

Lean4

/-- A normal closure is always normal. -/
theorem normal [h : IsNormalClosure F K L] : Normal F L :=
  Normal.of_algEquiv topEquiv (h :=
    h.adjoin_rootSet ▸
      IntermediateField.normal_iSup (h := fun _ ↦
        Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField <| h.splits _)))

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