∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℤ),
  (NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv v) ↑n ≤ 1