valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X

English

If the valuation v on RatFunc(K) satisfies 1 < v( RatFunc.X ), and p ∈ K[X] is nonzero, then v(p) = v(RatFunc.X)^{natDegree(p)}.

Русский

Если на RatFunc(K) выполнено 1 < v(X) и p ∈ K[X] ненулен, то v(p) = v(X)^{natDegree(p)}.

LaTeX

$$$\forall p\in K[X],\; p\neq 0 \Rightarrow 1 < v(\mathrm{X}) \Rightarrow v(p) = v(\mathrm{X})^{\operatorname{natDegree}(p)}$$$

Lean4

/-- If a valuation `v` is trivial on constants and `1 < v RatFunc.X` then for every polynomial `p`,
`v p = v RatFunc.X ^ p.natDegree`.

Note: The condition `1 < v RatFunc.X` is typically satisfied by the valuation at infinity. -/
theorem valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (hlt : 1 < v RatFunc.X) {p : K[X]} (hp : p ≠ 0) :
    v p = v RatFunc.X ^ p.natDegree :=
  by
  convert valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X K (RatFunc K) hv RatFunc.X hlt hp
  ext p
  nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)]
  exact (aeval_algebraMap_apply (RatFunc K) X p).symm

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