∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊥ →
    P.IsPrime →
      P ≠ ⊥ → p.ramificationIdx P = Multiset.count P (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p))