Theorems · Theorem · number theory

Ideal.sum_ramification_inertia

Deprecated since 2026-07-01Mathlib marks this declaration as deprecated.

∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L] [IsDedekindDomain R]
  [inst_7 : Algebra R K] [IsFractionRing R K] [inst_9 : Algebra S L] [IsFractionRing S L] [inst_11 : Algebra K L]
  [inst_12 : Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal],
  p ≠ ⊥ → ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P = Module.finrank K L

The fundamental identity of ramification index e and inertia degree f: for P ranging over the primes lying over p, ∑ P, e P * f P = [Frac(S) : Frac(R)]; here S is a finite R-module (and thus Frac(S) : Frac(R) is a finite extension) and p is maximal.

Defined in

Mathlib.NumberTheory.RamificationInertia.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDedekindDomainFieldFieldIsDedekindDomainAlgebraIsFractionRingAlgebraIsFractionRingAlgebraAlgebraIsScalarTowerIsScalarTowerModule.FiniteIdeal.IsMaximal