Theorems · Definition · number theory

ValuationSubring.inertiaSubgroup

(K : Type u_1) →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (A : ValuationSubring L) → Subgroup ↥(ValuationSubring.decompositionSubgroup K A)

The inertia subgroup defined as the kernel of the group homomorphism from the decomposition subgroup to the group of automorphisms of the residue field of A.

Defined in

Mathlib.RingTheory.Valuation.RamificationGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra