TODO: Add doc-string.

theorem NumberField.Odlyzko.tendsto_sum_idealNormCount_div (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, ↑(idealNormCount K k)) / ↑n) Filter.atTop (nhds (dedekindZeta_residue K))

theorem NumberField.Odlyzko.lSeriesSummable_idealNormCount (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun (n : ℕ) => ↑(idealNormCount K n)) s

theorem NumberField.Odlyzko.hasSum_dedekindZeta (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : HasSum (LSeries.term (fun (n : ℕ) => ↑(idealNormCount K n)) s) (dedekindZeta K s)