valuation_exists_uniformizer — Mathlib

English

There exists an element π in K whose v-adic valuation equals the canonical uniformizer value, namely Multiplicative.ofAdd(-1).

Русский

Существует элемент π в K такой, что его v-адическая оценка равна величине униформизатора, то есть Multiplicative.ofAdd(-1).

LaTeX

$$∃π ∈ K, v.valuation_K(π) = Multiplicative.ofAdd(-1 : ℤ)$$

Lean4

/-- There exists `π ∈ K` with `v`-adic valuation `Multiplicative.ofAdd (-1)`. -/
theorem valuation_exists_uniformizer : ∃ π : K, v.valuation K π = Multiplicative.ofAdd (-1 : ℤ) :=
  by
  obtain ⟨r, hr⟩ := v.intValuation_exists_uniformizer
  use algebraMap R K r
  rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]
  exact hr

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