exists_ne_zero_mem_ringOfIntegers_lt

English

A version of the ideal-lattice bound, but with a ∈ 𝓞(K) (ring of integers) under a Minkowski-type hypothesis, yielding a bound at all infinite places.

Русский

Версия не нулевого элемента в кольце целых 𝓞(K) при предположении Минковского, приводящая границы на всех бесконечных местах.

LaTeX

$$$\exists a \in \mathcal{O}_K,\ a \neq 0 \land \forall w:\ InfinitePlace\ K,\ w a < f w$$$

Lean4

/-- A version of `exists_ne_zero_mem_ideal_lt` for the ring of integers of `K`. -/
theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowskiBound K ↑1 < volume (convexBodyLT K f)) :
    ∃ a : 𝓞 K, a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w :=
  by
  obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt K (↑1) h
  obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
  exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Похожие утверждения