English
Let I be a fractional ideal and B a real bound with minkowskiBound(K,I) ≤ volume(convexBodySum(K,B)). Then there exists a ∈ I, a ≠ 0 with |N_Q(a)| ≤ (B / d)^d, where d = finrank_Q K.
Русский
Пусть I — дробный идеал, B — вещественное ограничение с Minkowski bound меньшe или равной объему convexBodySum. Тогда существует a ∈ I, a ≠ 0, такое что |N_Q(a)| ≤ (B/d)^d, где d = finsrank_Q K.
LaTeX
$$$\exists a \in I,\ a \neq 0 \land |\operatorname{Norm}_{\mathbb{Q}}(a)| \le (\frac{B}{\operatorname{finrank}_{\mathbb{Q}}K})^{\operatorname{finrank}_{\mathbb{Q}}K}$$$
Lean4
theorem exists_primitive_element_lt_of_isReal {w₀ : InfinitePlace K} (hw₀ : IsReal w₀) {B : ℝ≥0}
(hB : minkowskiBound K ↑1 < convexBodyLTFactor K * B) :
∃ a : 𝓞 K, ℚ⟮(a : K)⟯ = ⊤ ∧ ∀ w : InfinitePlace K, w a < max B 1 := by
classical
have : minkowskiBound K ↑1 < volume (convexBodyLT K (fun w ↦ if w = w₀ then B else 1)) :=
by
rw [convexBodyLT_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
simp_rw [ite_pow, one_pow]
rw [Finset.prod_ite_eq']
simp_rw [Finset.notMem_erase, ite_false, mult, hw₀, ite_true, one_mul, pow_one]
exact hB
obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this
refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩
· exact is_primitive_element_of_infinitePlace_lt h_nz (fun w h_ne ↦ by convert (if_neg h_ne) ▸ h_le w) (Or.inl hw₀)
· split_ifs <;> simp
