normalClosure — Mathlib

English

Let k ⊆ F ⊆ E be a tower of field extensions with F/k Galois. Then the normal closure of K over k in F is Galois over k.

Русский

Пусть k ⊆ F ⊆ E образуют цепь расширений полей и F/k галуа. Тогда нормальное замыкание K над k внутри F — галуа над k.

LaTeX

$$$\text{If } F/k \text{ is Galois, then } \operatorname{normalClosure}_k(K|F)/k \text{ is Galois}$$$

Lean4

/-- Let $F / K / k$ be a tower of field extensions. If $F$ is Galois over $k$,
then the normal closure of $K$ over $k$ in $F$ is Galois over $k$. -/
@[stacks 0EXM]
instance normalClosure : IsGalois k (normalClosure k K F) where
  to_isSeparable := Algebra.isSeparable_tower_bot_of_isSeparable k _ F

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