Coefficients

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.idealNormCount (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ℕ

An ideal norm count used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealNormCount K n = Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

theorem NumberField.Odlyzko.dedekindZeta_eq_LSeries_idealNormCount (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : dedekindZeta K s = LSeries (fun (n : ℕ) => ↑(idealNormCount K n)) s