TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.codifferentClass (K : Type u_1) [Field K] [NumberField K] : ClassGroup (RingOfIntegers K)

A codifferent class used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.codifferentClass K = (ClassGroup.mk K) (NumberField.Odlyzko.traceDualIdealUnit K 1)

theorem NumberField.Odlyzko.mk_traceDualIdealUnit (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : (ClassGroup.mk K) (traceDualIdealUnit K I) = codifferentClass K * ((ClassGroup.mk K) I)⁻¹

noncomputable def NumberField.Odlyzko.traceDualClassEquiv (K : Type u_1) [Field K] [NumberField K] : ClassGroup (RingOfIntegers K) ≃ ClassGroup (RingOfIntegers K)

A trace dual class equiv used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.classGroupInvEquiv (K : Type u_1) [Field K] : ClassGroup (RingOfIntegers K) ≃ ClassGroup (RingOfIntegers K)

A class group inv equiv used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.traceDualInverseClassEquiv (K : Type u_1) [Field K] [NumberField K] : ClassGroup (RingOfIntegers K) ≃ ClassGroup (RingOfIntegers K)

A trace dual inverse class equiv used in the Odlyzko-bound argument.

Equations

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

@[simp]

theorem NumberField.Odlyzko.traceDualInverseClassEquiv_apply (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) : (traceDualInverseClassEquiv K) C = ((traceDualClassEquiv K) C⁻¹)⁻¹

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