Documentation

LeanPool.Odlyzko.DedekindZeta.PrimeIdealFactor

TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.primeIdealNorm (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

A prime ideal norm used in the Odlyzko-bound argument.

Equations

NumberField.Odlyzko.primeIdealNorm K P = Ideal.absNorm P.asIdeal

Instances For

theorem NumberField.Odlyzko.one_lt_primeIdealNorm (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) :

1 < primeIdealNorm K P

noncomputable def NumberField.Odlyzko.primeIdealFactor (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (s : ℂ) :

A prime ideal factor used in the Odlyzko-bound argument.

Equations

NumberField.Odlyzko.primeIdealFactor K P s = NumberField.Odlyzko.localFactor (NumberField.Odlyzko.primeIdealNorm K P) s

Instances For

theorem NumberField.Odlyzko.primeIdealFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {s : ℂ} (hs : 0 < s.re) :

primeIdealFactor K P s ≠ 0