{A : Type u_4} →
  [inst : CommRing A] →
    (p : Ideal A) →
      [hpm : p.IsMaximal] →
        (B : Type u_5) →
          [inst_1 : CommRing B] →
            [IsDedekindDomain B] →
              [inst_3 : Algebra A B] →
                [IsDomain A] → [Module.IsTorsionFree A B] → [Algebra.IsIntegral A B] → Fintype ↑(p.primesOver B)