classical
rw [primesOverFinset, Ideal.map_bot, ← Ideal.zero_eq_bot, factors_zero]
rfl
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ primesOverFinset S ⊥ = ∅
no goals