Theorems · Definition · field theory

InfiniteGalois.normalAutEquivQuotient

{k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            (H : ClosedSubgroup Gal(K/k)) →
              [inst_4 : (↑H).Normal] → Gal(K/k) ⧸ ↑H ≃* Gal(↥(IntermediateField.fixedField ↑H)/k)

If H is a closed normal subgroup of Gal(K / k), then Gal(fixedField H / k) is isomorphic to Gal(K / k) ⧸ H.

Defined in

Mathlib.FieldTheory.Galois.Infinite

Cited by

1 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraIsGaloisSubgroup.Normal