exists_isUniformizer_of_isCyclic_of_nontrivial

English

If two elements are uniformizers, they are associated.

Русский

Если два элемента являются uniformizers, они ассоциированы.

LaTeX

$$v.IsUniformizer π₁ ∧ v.IsUniformizer π₂ → Associated π₁ π₂$$

Lean4

theorem exists_isUniformizer_of_isCyclic_of_nontrivial : ∃ π : K₀, IsUniformizer v (π : K) :=
  by
  simp only [IsUniformizer.iff, Subtype.exists, mem_valuationSubring_iff, exists_prop]
  set g := (valueGroup v).genLTOne with hg
  obtain ⟨⟨π, hπ⟩, hγ0⟩ : g.1 ∈ ((range v) \ {0}) :=
    by
    rw [← valueGroup_eq_range, hg]
    exact mem_image_of_mem Units.val (valueGroup v).genLTOne_mem
  use π
  rw [hπ, hg]
  exact ⟨le_of_lt (valueGroup v).genLTOne_lt_one, by rw [valueGroup_genLTOne_eq_generator]⟩

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