∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : IsDedekindDomain S]
  [inst_3 : Algebra R 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 ∈ primesOverFinset p S, Ideal.ramificationIdx (algebraMap R S) p P * p.inertiaDeg P = Module.finrank K L