exists_unitSMul_mem_integerSet — Mathlib

English

If x ≠ 0 and x lies in the image of the algebra map, there exists a unit u such that u · x ∈ integerSet(K).

Русский

Если x ≠ 0 и лежит в образе алгебраического отображения, существует единица u такая, что u·x ∈ integerSet(K).

LaTeX

$$If x ≠ 0 and x ∈ mixedEmbedding K '' Set.range (algebraMap (𝓞 K) K) then ∃ u ∈ (𝓞 K)ˣ, u • x ∈ integerSet K.$$

Lean4

/-- If `x : mixedSpace K` is nonzero and the image of an algebraic integer, then there exists a
unit such that `u • x ∈ integerSet K`. -/
theorem exists_unitSMul_mem_integerSet {x : mixedSpace K} (hx : x ≠ 0)
    (hx' : x ∈ mixedEmbedding K '' (Set.range (algebraMap (𝓞 K) K))) : ∃ u : (𝓞 K)ˣ, u • x ∈ integerSet K :=
  by
  replace hx : mixedEmbedding.norm x ≠ 0 :=
    (norm_eq_zero_iff' (Set.mem_range_of_mem_image (mixedEmbedding K) _ hx')).not.mpr hx
  obtain ⟨u, hu⟩ := exists_unit_smul_mem hx
  obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx'
  exact ⟨u, mem_integerSet.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_mul]⟩⟩

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