tower_top_of_isGalois — Mathlib

English

If E/K/F is a tower of fields and E is Galois over F, then E is Galois over K.

Русский

Если поля F ⊆ K ⊆ E и E/GF галуа над F, то E галуа над K.

LaTeX

$$IsGalois K E$$

Lean4

/-- Let $E / K / F$ be a tower of field extensions.
If $E$ is Galois over $F$, then $E$ is Galois over $K$. -/
@[stacks 09I2]
theorem tower_top_of_isGalois [IsGalois F E] : IsGalois K E :=
  { to_isSeparable := Algebra.isSeparable_tower_top_of_isSeparable F K E
    to_normal := Normal.tower_top_of_normal F K E }

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