Theorems · Theorem · number theory

IsInertiaField.of_isGaloisGroup

∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (G : Type u_7) [inst_7 : Group G] [Finite G] [inst_9 : MulSemiringAction G L]
  [IsGaloisGroup G K L] [inst_11 : MulSemiringAction G B] [inst_12 : Algebra B L] [IsFractionRing B L]
  [SMulDistribClass Gal(L/K) B L] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(Ideal.inertia G P)) E L],
  IsInertiaField K L P E

If G is a Galois group for L/K and the inertia group of P in G is a Galois group for L/E, then E is an inertia field for P.

Defined in

Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraCommRingFieldAlgebraMulSemiringActionGroupFiniteMulSemiringActionIsGaloisGroupMulSemiringActionAlgebraIsFractionRingSMulDistribClassSMulDistribClassIsGaloisGroup