TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.unitExponentReindex (K : Type u_1) [Field K] [NumberField K] : (Fin (Units.rank K) → ℤ) ≃ ({ w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ)

An unit exponent reindex used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.fundamentalUnitForShift_unitExponentReindex (K : Type u_1) [Field K] [NumberField K] (f : Fin (Units.rank K) → ℤ) : fundamentalUnitForShift ((unitExponentReindex K) f) = ∏ i : Fin (Units.rank K), Units.fundSystem K i ^ f i

noncomputable def NumberField.Odlyzko.unitDecompositionMap (K : Type u_1) [Field K] [NumberField K] : ↥(Units.torsion K) × ({ w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) → (RingOfIntegers K)ˣ

An unit decomposition map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitDecompositionMap K p = ↑p.1 * NumberField.Odlyzko.fundamentalUnitForShift p.2

theorem NumberField.Odlyzko.bijective_unitDecompositionMap (K : Type u_1) [Field K] [NumberField K] : Function.Bijective (unitDecompositionMap K)

noncomputable def NumberField.Odlyzko.unitDecompositionEquiv (K : Type u_1) [Field K] [NumberField K] : ↥(Units.torsion K) × ({ w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) ≃ (RingOfIntegers K)ˣ

An unit decomposition equiv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitDecompositionEquiv K = Equiv.ofBijective (NumberField.Odlyzko.unitDecompositionMap K) ⋯

@[simp]

theorem NumberField.Odlyzko.unitDecompositionEquiv_apply (K : Type u_1) [Field K] [NumberField K] (p : ↥(Units.torsion K) × ({ w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ)) : (unitDecompositionEquiv K) p = ↑p.1 * fundamentalUnitForShift p.2