∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Nontrivial S] [inst_2 : IsDedekindDomain S] [inst_3 : Module.Free ℤ S]
  [Module.Finite ℤ S] {I : Ideal S}, 0 < Ideal.absNorm I ↔ I ∈ nonZeroDivisors (Ideal S)