A packing estimate using the separation of distinct algebraic integers. It is uniform in the number field, including fields of degree one, and does not require a lower bound on the radius in terms of the discriminant.

theorem CCDN.boundedArchimedeanIntegers_separated_count (K : Type u_1) [Field K] [NumberField K] {B : ℝ} (hB : 0 ≤ B) : ↑(boundedArchimedeanIntegers K B).ncard ≤ (2 * √↑(Module.finrank ℚ K) * B + 1) ^ Module.finrank ℚ K

For B ≥ 0, the number of algebraic integers of K bounded by B at every infinite place is at most (2 * √n * B + 1) ^ n, where n = [K : ℚ].