Theorems · Theorem · field theory

IntermediateField.fixingSubgroup_isClosed

∀ {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], IsClosed ↑E.fixingSubgroup

Given a tower of fields L/E/K, with E/K finite, the subgroup Gal(L/E) ≤ Gal(L/K) is closed.

Defined in

Mathlib.FieldTheory.KrullTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensional