English
For f ∈ Polynomial K and g ≠ 0, the valuation of RatFunc.mk f g equals intValuation f divided by intValuation g, consistent with mk' representation.
Русский
Для f ∈ Polynomial K и g ≠ 0, valuation RatFunc.mk f g равна intValuation f / intValuation g (совместимо через mk').
LaTeX
$$$ \mathrm{Valuation}.instFunLike.coe (\mathrm{IsDedekindDomain.HeightOneSpectrum.valuation } (\mathrm{RatFunc } K) (\mathrm{Polynomial.idealX } K)) (\mathrm{RatFunc.mk } f g) = \frac{\mathrm{polynomial.intValuation} f}{\mathrm{polynomial.intValuation} g} $$$
Lean4
theorem valuation_of_mk (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :
(Polynomial.idealX K).valuation _ (RatFunc.mk f g) =
(Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g :=
by simp only [RatFunc.mk_eq_mk' _ hg, valuation_of_mk']
