Theorems · Definition · field theory

FiniteGaloisIntermediateField.adjoin

(k : Type u_1) →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] → [IsGalois k K] → (s : Set K) → [Finite ↑s] → FiniteGaloisIntermediateField k K

The minimal (finite) Galois intermediate field containing a finite set s : Set K in a Galois extension K/k defined as the normal closure of the field obtained by adjoining the set s : Set K to k.

Defined in

Mathlib.FieldTheory.Galois.GaloisClosure

Cited by

11 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGaloisFinite