English
Under certain lt-one conditions at an infinite place w, x in the ring of integers generates the field as a primitive element.
Русский
При определённых условиях lt вокруг бесконечной точки w элемент x порождает поле как примитивный элемент.
LaTeX
$$$\text{Theorem }\mathbb{Q}\langle x \rangle = \mathbb{C}$ under LT-like hypotheses$$
Lean4
theorem one_le_of_lt_one {w : InfinitePlace K} {a : (𝓞 K)} (ha : a ≠ 0) (h : ∀ ⦃z⦄, z ≠ w → z a < 1) : 1 ≤ w a :=
by
suffices (1 : ℝ) ≤ |Algebra.norm ℚ (a : K)| by
contrapose! this
rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
refine Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty
· exact pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _
· refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
by_cases hz : z = w
· rwa [hz]
· exact h hz
rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr ha)
