Theorems · Definition · field theory

IsGaloisGroup.intermediateFieldEquivSubgroup

(G : Type u_1) →
  (K : Type u_3) →
    (L : Type u_4) →
      [inst : Group G] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra K L] →
              [inst_4 : MulSemiringAction G L] →
                [hGKL : IsGaloisGroup G K L] → [Finite G] → IntermediateField K L ≃o (Subgroup G)ᵒᵈ

The Galois correspondence from intermediate fields to subgroups.

Defined in

Mathlib.FieldTheory.Galois.IsGaloisGroup

Cited by

6 results in Mathlib

Foundations

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

Assumes

GroupFieldFieldAlgebraMulSemiringActionIsGaloisGroupFinite