TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.CompletedZeta.discriminantFactor (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℂ

A discriminant factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.CompletedZeta.discriminantFactor K s = ↑|↑(NumberField.discr K)| ^ (s / 2)

noncomputable def NumberField.Odlyzko.CompletedZeta.archimedeanFactor (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℂ

An archimedean factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.CompletedZeta.archimedeanFactor K s = s.Gammaℝ ^ NumberField.InfinitePlace.nrRealPlaces K * (s.Gammaℂ / 2) ^ NumberField.InfinitePlace.nrComplexPlaces K

noncomputable def NumberField.Odlyzko.CompletedZeta.completed (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℂ

A completed used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.discr_abs_pos (K : Type u_1) [Field K] [NumberField K] : 0 < |↑(discr K)|

theorem NumberField.Odlyzko.dedekindDiscriminantFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : CompletedZeta.discriminantFactor K s ≠ 0

theorem NumberField.Odlyzko.differentiable_dedekindDiscriminantFactor (K : Type u_1) [Field K] [NumberField K] : Differentiable ℂ (CompletedZeta.discriminantFactor K)