Theorems · Theorem · field theory

IntermediateField.fixingSubgroup_isOpen

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  [FiniteDimensional K ↥E], IsOpen ↑E.fixingSubgroup

Let L/E/K be a tower of fields with E/K finite. Then Gal(L/E) is an open subgroup of Gal(L/K).

Defined in

Mathlib.FieldTheory.KrullTopology

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensional