Theorems · Theorem · field theory

IsGaloisGroup.of_isScalarTower

∀ (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] [Finite G] [IsGaloisGroup G K L] (E : Type u_5)
  [inst_7 : Field E] [inst_8 : Algebra K E] [inst_9 : Algebra E L] [IsScalarTower K E L],
  IsGaloisGroup (↥(fixingSubgroup G (Set.range ⇑(algebraMap E L)))) E L

If G is a Galois group on L/K and L/E/K is a tower of field extensions, then the fixing subgroup of the image of E in L is a Galois group on L/E.

Defined in

Mathlib.FieldTheory.Galois.IsGaloisGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupFieldFieldAlgebraMulSemiringActionFiniteIsGaloisGroupFieldAlgebraAlgebraIsScalarTower