isGalois — Mathlib

English

If E is normal over F, then the separable closure of F in E is Galois over F.

Русский

Если E нормально над F, то separableClosure F E над F является Галуа-разветвлением.

LaTeX

$$IsGalois F (separableClosure F E)$$

Lean4

/-- If `E` is normal over `F`, then the separable closure of `F` in `E` is Galois (i.e.
normal and separable) over `F`. -/
@[stacks 0EXK]
instance isGalois [Normal F E] : IsGalois F (separableClosure F E)
    where
  to_isSeparable := separableClosure.isSeparable F E
  to_normal := by
    rw [← separableClosure.normalClosure_eq_self]
    exact normalClosure.normal F _ E

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