English
For any Laurent series x, there exists a rational function f such that the valuation v(f) matches the valuation v(x).
Русский
Для любой редуцированной Лаурентовой серии x существует рациональная функция f такая, что v(f) = v(x).
LaTeX
$$$\exists f : RatFunc K, Valued.v f = Valued.v x$$$
Lean4
theorem val_le_one_iff_eq_coe (f : K⸨X⸩) : Valued.v f ≤ (1 : ℤᵐ⁰) ↔ ∃ F : K⟦X⟧, F = f :=
by
rw [valuation_le_iff_coeff_lt_log_eq_zero _ one_ne_zero, log_one, neg_zero]
refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩
on_goal 1 => ext (_ | n)
· simp only [Int.ofNat_eq_coe, coeff_coe_powerSeries, coeff_mk]
on_goal 1 => simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]
on_goal 2 => rintro ⟨F, rfl⟩ _ _
all_goals
apply HahnSeries.embDomain_notin_range
simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk, Set.mem_range, not_exists,
reduceCtorEq]
intro
· simp only [not_false_eq_true]
· cutsat
