exists_ratFunc_eq_v — Mathlib

English

Every Laurent series is the value of some RatFunc under the valuation.

Русский

Каждый лаурентовый ряд является значением некоторой рациональной функции под валидацией.

LaTeX

$$$\exists f : RatFunc K, Valued.v f = Valued.v x$$$

Lean4

theorem exists_ratFunc_eq_v (x : K⸨X⸩) : ∃ f : RatFunc K, Valued.v f = Valued.v x :=
  by
  by_cases hx : Valued.v x = 0
  · use 0
    simp [hx]
  use RatFunc.X ^ (-WithZero.log (Valued.v x))
  rw [zpow_neg, map_inv₀, map_zpow₀, v_def, valuation_X_eq_neg_one, ← WithZero.exp_zsmul, ← WithZero.exp_neg]
  simp [WithZero.exp_log, hx]

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