valuation_LaurentSeries_equal_extension

English

The X-adic valuation of Laurent series, extended along the dense embedding, agrees with the valuation on the Laurent series completion.

Русский

Ценность, связанная с X-адическим завершением Лорентовых рядов, совпадает с ценностью на завершение самих рядов.

LaTeX

$$$(\\mathrm{LaurentSeriesPkg}\\,K).\\mathrm{isDenseInducing}.\\mathrm{extend}\\ \\mathrm{Valued.v} = \\mathrm{Valued.v}$$$

Lean4

theorem valuation_LaurentSeries_equal_extension :
    (LaurentSeriesPkg K).isDenseInducing.extend Valued.v = (Valued.v : K⸨X⸩ → ℤᵐ⁰) :=
  by
  apply IsDenseInducing.extend_unique
  · intro x
    rw [v_def, valuation_eq_LaurentSeries_valuation K x]
    rfl
  · exact Valued.continuous_valuation (K := K⸨X⸩)

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