English
Under a Minkowski-type bound h for (K,I), there exists a primitive element a ∈ 𝓞(K) with w(a) < f(w) for all infinite places w, including an added constraint when w0 is fixed complex place.
Русский
При условии Минковского типа h существует примитивный элемент a ∈ 𝓞(K) такой, что w(a) < f(w) на всех бесконечных местах, включая дополнительное ограничение для фиксированного комплексного места w0.
LaTeX
$$$\exists a \in \mathcal{O}_K,\ a \neq 0 \land (∀ w, w \neq w_0 \Rightarrow w a < f w) \land |(w_0.visual embedding(a)).re| < 1 \land |(w_0.visual embedding(a)).im| < (f(w_0))^2$$$
Lean4
/-- A version of `exists_ne_zero_mem_ideal_lt'` for the ring of integers of `K`. -/
theorem exists_ne_zero_mem_ringOfIntegers_lt' (w₀ : { w : InfinitePlace K // IsComplex w })
(h : minkowskiBound K ↑1 < volume (convexBodyLT' K f w₀)) :
∃ a : 𝓞 K,
a ≠ 0 ∧
(∀ w : InfinitePlace K, w ≠ w₀ → w a < f w) ∧
|(w₀.val.embedding a).re| < 1 ∧ |(w₀.val.embedding a).im| < (f w₀ : ℝ) ^ 2 :=
by
obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt' K (↑1) w₀ h
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩
