TODO: Add doc-string.

theorem NumberField.Odlyzko.dedekindArchimedeanFactor_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : CompletedZeta.archimedeanFactor K s = (s.Gammaℂ / 2) ^ InfinitePlace.nrComplexPlaces K

theorem NumberField.Odlyzko.completedDedekindZeta_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : CompletedZeta.completed K s = CompletedZeta.discriminantFactor K s * (s.Gammaℂ / 2) ^ InfinitePlace.nrComplexPlaces K * dedekindZeta K s

theorem NumberField.Odlyzko.two_mul_nrComplexPlaces_eq_finrank (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : 2 * InfinitePlace.nrComplexPlaces K = Module.finrank ℚ K

theorem NumberField.Odlyzko.logDeriv_dedekindArchimedeanFactor_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 0 < s.re) : logDeriv (CompletedZeta.archimedeanFactor K) s = ↑(InfinitePlace.nrComplexPlaces K) * (s.digamma - Complex.log (2 * ↑Real.pi))