∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Filter.Tendsto (fun s => ↑(Nat.card { I // ↑(Ideal.absNorm I) ≤ s }) / s) Filter.atTop
    (nhds
      (2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
            NumberField.Units.regulator K *
          ↑(NumberField.classNumber K) /
        (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|)))