Commit 2024-02-19 09:46 c1e6b9cb

feat: Add NumberField.is_primitive_element_of_infinitePlace_lt (#10033) Prove the following

theorem NumberField.is_primitive_element_of_infinitePlace_lt (x : 𝓞 K)
     {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w'⦄, w' ≠ w → w' x < 1)
     (h₃ : IsReal w ∨ |(w.embedding x).re| < 1) : ℚ⟮(x:K)⟯ = ⊤ := by

If the place w is not real, we need the condition |(w.embedding x).re| < 1 to ensure x is not a real number at the place w.