TODO: Add doc-string.

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

A trace dual ideal unit used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.traceDualIdealUnit K I = Units.mk0 (FractionalIdeal.dual ℤ ℚ ↑I) ⋯

@[simp]

theorem NumberField.Odlyzko.coe_traceDualIdealUnit (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ↑(traceDualIdealUnit K I) = FractionalIdeal.dual ℤ ℚ ↑I

@[simp]

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

theorem NumberField.Odlyzko.coe_traceDualIdealUnit_eq_dual_one_mul_inv (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ↑(traceDualIdealUnit K I) = FractionalIdeal.dual ℤ ℚ 1 * (↑I)⁻¹

theorem NumberField.Odlyzko.absNorm_traceDualIdealUnit (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : FractionalIdeal.absNorm ↑(traceDualIdealUnit K I) = FractionalIdeal.absNorm (FractionalIdeal.dual ℤ ℚ 1) * (FractionalIdeal.absNorm ↑I)⁻¹

theorem NumberField.Odlyzko.absNorm_traceDual_one (K : Type u_1) [Field K] [NumberField K] : FractionalIdeal.absNorm (FractionalIdeal.dual ℤ ℚ 1) = |↑(discr K)|⁻¹