TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.fractionalIdealElementUnitMulEquiv (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (u : (RingOfIntegers K)ˣ) : ↥↑↑I ≃ ↥↑↑I

A fractional ideal element unit mul equiv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fractionalIdealElementUnitMulEquiv K I u = { toFun := fun (x : ↥↑↑I) => ⟨↑↑u * ↑x, ⋯⟩, invFun := fun (x : ↥↑↑I) => ⟨↑↑u⁻¹ * ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem NumberField.Odlyzko.complexPlaceGaussian_mul_unit (K : Type u_1) [Field K] [NumberField K] (u : (RingOfIntegers K)ˣ) (x : K) (q : InfinitePlace K → ℝ) : complexPlaceGaussian K x ((fun (w : InfinitePlace K) => w ↑↑u) * q) = complexPlaceGaussian K (↑↑u * x) q

theorem NumberField.Odlyzko.fractionalShapeIdealTheta_add_unitCoordinateShift (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (y : mixedEmbedding.realSpace K) (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : fractionalShapeIdealTheta K I (↑mixedEmbedding.fundamentalCone.expMapBasis (y + unitCoordinateShift z)) ⋯ = fractionalShapeIdealTheta K I (↑mixedEmbedding.fundamentalCone.expMapBasis y) ⋯