Theorems · Theorem · number theory

NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {f : NumberField.InfinitePlace K → NNReal}
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) →
    ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(f w)

Let I be a fractional ideal of K. Assume that f : InfinitePlace K → ℝ≥0 is such that minkowskiBound K I < volume (convexBodyLT K f) where convexBodyLT K f is the set of points x such that ‖x w‖ < f w for all infinite places w (see convexBodyLT_volume for the computation of this volume), then there exists a nonzero algebraic number a in I such that w a < f w for all infinite places w.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Cited by

1 results in Mathlib

Foundations

Depth 311 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField