adjoin_eq_top_of_infinitePlace_lt

English

The previous LT condition implies that the ℚ-adjoin of x equals the top subfield.

Русский

Условие LT влечёт, что надполе, порождаемое x над полем ℚ, совпадает с верхней подполя.

LaTeX

$$$\text{adjoin }\mathbb{Q}\{x\} = \top$$$

Lean4

theorem _root_.NumberField.adjoin_eq_top_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) : Algebra.adjoin ℚ {(x : K)} = ⊤ :=
  by
  rw [← IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite ℚ _)]
  exact congr_arg IntermediateField.toSubalgebra <| NumberField.is_primitive_element_of_infinitePlace_lt h₁ h₂ h₃

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