exists_unit_smul_mem — Mathlib

English

If the norm of x is nonzero, there exists a unit u in the ring of integers such that u · x lies in the fundamental cone.

Русский

Если норма x не равна нулю, существует единица u в кольце целых чисел, такая что u·x лежит в фундаментальном конусе.

LaTeX

$$∀ x, if \currenthx : mixedEmbedding.norm x ≠ 0, then ∃ u ∈ (𝓞 K)ˣ, u·x ∈ fundamentalCone(K).$$

Lean4

theorem exists_unit_smul_mem (hx : mixedEmbedding.norm x ≠ 0) : ∃ u : (𝓞 K)ˣ, u • x ∈ fundamentalCone K := by
  classical
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
  · exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
  · obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
    exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

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