TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.fractionalShapeCovolumeConstant (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ℝ

A fractional shape covolume constant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fractionalShapeCovolumeConstant K I = ↑(FractionalIdeal.absNorm ↑I) * √|↑(NumberField.discr K)|

theorem NumberField.Odlyzko.fractionalShapeCovolumeConstant_traceDual (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : fractionalShapeCovolumeConstant K (traceDualIdealUnit K I) = (fractionalShapeCovolumeConstant K I)⁻¹