∀ (R : Type u_1) [inst : CommRing R] (N : Type u_3) [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  [inst_3 : IsLocalRing R],
  Module.supportDim R N = 0 → Module.support R N = PrimeSpectrum.zeroLocus ↑(IsLocalRing.maximalIdeal R)