∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (p : Ideal R) [inst_2 : Algebra R S]
  (K : Type u_1) [inst_3 : Field K] [inst_4 : Algebra R K] (L : Type u_2) [inst_5 : Field L] [inst_6 : Algebra S L]
  [IsFractionRing S L] [hRK : IsFractionRing R K] [IsDomain S] [IsDedekindDomain R] [inst_10 : Algebra K L]
  [inst_11 : Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S],
  Module.finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = Module.finrank K L