TODO: Add doc-string.

@[reducible, inline]

abbrev NumberField.Odlyzko.unitShiftIndex (K : Type u_1) [Field K] [NumberField K] : Type u_1

An unit shift index used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitShiftIndex K = ({ w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } → ℤ)

theorem NumberField.Odlyzko.fundamentalUnitForShift_add (K : Type u_1) [Field K] [NumberField K] (z z' : unitShiftIndex K) : fundamentalUnitForShift (z + z') = fundamentalUnitForShift z * fundamentalUnitForShift z'

@[simp]

theorem NumberField.Odlyzko.fundamentalUnitForShift_zero (K : Type u_1) [Field K] [NumberField K] : fundamentalUnitForShift 0 = 1

@[simp]

theorem NumberField.Odlyzko.fundamentalUnitForShift_neg (K : Type u_1) [Field K] [NumberField K] (z : unitShiftIndex K) : fundamentalUnitForShift (-z) = (fundamentalUnitForShift z)⁻¹

@[reducible, inline]

abbrev NumberField.Odlyzko.nonzeroIdealElement (K : Type u_1) [Field K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Type u_1

A nonzero ideal element used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.nonzeroIdealElement K J = { x : NumberField.RingOfIntegers K // x ∈ ↑J ∧ x ≠ 0 }

noncomputable def NumberField.Odlyzko.idealSetInteger (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : RingOfIntegers K

An ideal set integer used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealSetInteger K J a = ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet ↑((NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv K J) a))

theorem NumberField.Odlyzko.idealSetInteger_mem (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : idealSetInteger K J a ∈ ↑J

theorem NumberField.Odlyzko.idealSetInteger_ne_zero (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : idealSetInteger K J a ≠ 0

theorem NumberField.Odlyzko.idealSetInteger_injective (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Function.Injective (idealSetInteger K J)

noncomputable def NumberField.Odlyzko.idealElementDecompositionMap (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K → nonzeroIdealElement K J

An ideal element decomposition map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealElementDecompositionMap K J p = ⟨↑(NumberField.Odlyzko.fundamentalUnitForShift p.2)⁻¹ * NumberField.Odlyzko.idealSetInteger K J p.1, ⋯⟩

@[simp]

theorem NumberField.Odlyzko.idealElementDecompositionMap_coe (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (p : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K) : ↑↑(idealElementDecompositionMap K J p) = (algebraMap (RingOfIntegers K) K) ↑(fundamentalUnitForShift p.2)⁻¹ * idealSetElement K J p.1

theorem NumberField.Odlyzko.injective_idealElementDecompositionMap (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Function.Injective (idealElementDecompositionMap K J)

theorem NumberField.Odlyzko.surjective_idealElementDecompositionMap (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Function.Surjective (idealElementDecompositionMap K J)

noncomputable def NumberField.Odlyzko.idealElementDecompositionEquiv (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K ≃ nonzeroIdealElement K J

An ideal element decomposition equiv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealElementDecompositionEquiv K J = Equiv.ofBijective (NumberField.Odlyzko.idealElementDecompositionMap K J) ⋯

@[simp]

theorem NumberField.Odlyzko.idealElementDecompositionEquiv_apply (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (p : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K) : (idealElementDecompositionEquiv K J) p = idealElementDecompositionMap K J p

def NumberField.Odlyzko.unitShiftNegEquiv (K : Type u_1) [Field K] [NumberField K] : unitShiftIndex K ≃ unitShiftIndex K

An unit shift neg equiv used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.idealElementMulDecompositionEquiv (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K ≃ nonzeroIdealElement K J

An ideal element mul decomposition equiv used in the Odlyzko-bound argument.

Equations

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

@[simp]

theorem NumberField.Odlyzko.idealElementMulDecompositionEquiv_coe (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (p : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K) : ↑↑((idealElementMulDecompositionEquiv K J) p) = (algebraMap (RingOfIntegers K) K) ↑(fundamentalUnitForShift p.2) * idealSetElement K J p.1