TODO: Add doc-string.

@[reducible, inline]

abbrev NumberField.Odlyzko.NonzeroIdeal (K : Type u_1) [Field K] : Type u_1

A nonzero ideal used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.NonzeroIdeal K = { I : Ideal (NumberField.RingOfIntegers K) // I ≠ 0 }

noncomputable def NumberField.Odlyzko.idealPrimeFactors (K : Type u_1) [Field K] [NumberField K] (I : NonzeroIdeal K) : Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))

An ideal prime factors used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.idealOfPrimeFactors (K : Type u_1) [Field K] (m : Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : NonzeroIdeal K

An ideal of prime factors used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealOfPrimeFactors K m = ⟨(Multiset.map IsDedekindDomain.HeightOneSpectrum.asIdeal m).prod, ⋯⟩

@[simp]

theorem NumberField.Odlyzko.idealOfPrimeFactors_coe (K : Type u_1) [Field K] (m : Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : ↑(idealOfPrimeFactors K m) = (Multiset.map IsDedekindDomain.HeightOneSpectrum.asIdeal m).prod

theorem NumberField.Odlyzko.idealOfPrimeFactors_idealPrimeFactors (K : Type u_1) [Field K] [NumberField K] (I : NonzeroIdeal K) : idealOfPrimeFactors K (idealPrimeFactors K I) = I

theorem NumberField.Odlyzko.idealPrimeFactors_idealOfPrimeFactors (K : Type u_1) [Field K] [NumberField K] (m : Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : idealPrimeFactors K (idealOfPrimeFactors K m) = m

noncomputable def NumberField.Odlyzko.nonzeroIdealEquivPrimeFactors (K : Type u_1) [Field K] [NumberField K] : NonzeroIdeal K ≃ Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))

A nonzero ideal equiv prime factors used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.nonzeroIdealEquivPrimeFactors K = { toFun := NumberField.Odlyzko.idealPrimeFactors K, invFun := NumberField.Odlyzko.idealOfPrimeFactors K, left_inv := ⋯, right_inv := ⋯ }