of_fixed_field — Mathlib

English

Let E be a field with a finite group G acting on E by automorphisms. Then E is a Galois extension of its fixed subfield E^G.

Русский

Пусть поле E имеет действие конечной группы G посредством автоморфизмов. Тогда расширение E над фиксированным полем E^G является Галуа-расширением.

LaTeX

$$IsGalois (FixedPoints.subfield G E) E$$

Lean4

/-- Let $E$ be a field. Let $G$ be a finite group acting on $E$.
Then the extension $E / E^G$ is Galois. -/
@[stacks 09I3 "first part"]
instance of_fixed_field (G : Type*) [Group G] [Finite G] [MulSemiringAction G E] :
    IsGalois (FixedPoints.subfield G E) E :=
  ⟨⟩

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