valuation_coe_ratFunc — Mathlib

English

Coefficients of RatFunc, when interpreted as LaurentSeries, align with the valuation map on LaurentSeries.

Русский

Коэффициенты RatFunc, интерпретируемые как Лорантовские ряды, согласованы со значением валюации Лорантовских рядов.

LaTeX

$$$\mathrm{valuation}(f) = \mathrm{valuation}(f)$$$

Lean4

@[simp]
theorem valuation_coe_ratFunc (f : RatFunc K) : Valued.v (f : K⸨X⸩) = Valued.v f := by
  simp [valuation_def, ← valuation_eq_LaurentSeries_valuation]

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