English
Let K be a field, Γ as above, and assume w ∈ L with v(w) > 1. For any nonzero polynomial p ∈ K[X], the valuation of p evaluated at w equals v(w) raised to the natDegree of p: v(p.aeval w) = v(w)^{natDegree(p)}.
Русский
Пусть K — поле, Γ — линейно упорядоченная группа, v — оценка на L, w ∈ L и v(w) > 1. Для любого ненулевого полинома p ∈ K[X] выполняется v(p(aeval w)) = v(w)^{natDegree(p)}.
LaTeX
$$$\forall w\in L,\; \forall p\in K[X],\; p\neq 0 \Rightarrow 1 < v(w) \Rightarrow v(p.\mathrm{aeval}\, w) = v(w)^{\operatorname{natDegree}(p)}$$$
Lean4
theorem valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (w : L) (hpos : 1 < v w) {p : Polynomial K}
(hp : p ≠ 0) : v (p.aeval w) = v w ^ p.natDegree :=
by
rw [← valuation_aeval_monomial_eq_valuation_pow _ _ hv _ _ ((leadingCoeff_ne_zero).mpr hp)]
nth_rw 1 [as_sum_range p, map_sum]
apply Valuation.map_sum_eq_of_lt _ (by simp) (by aesop)
intro i hi
simp only [Finset.mem_sdiff, Finset.mem_range, Nat.lt_add_one_iff, Finset.mem_singleton, ← lt_iff_le_and_ne] at hi
simp only [← C_mul_X_pow_eq_monomial, map_mul, aeval_C, map_pow, aeval_X, coeff_natDegree]
by_cases h0 : (p.coeff i) = 0
·
simp [h0, map_zero, zero_mul, one_mul, hv p.leadingCoeff ((leadingCoeff_ne_zero).mpr hp),
pow_pos (lt_trans zero_lt_one hpos) p.natDegree]
· simp [one_mul, hv p.leadingCoeff ((leadingCoeff_ne_zero).mpr hp), hv _ h0, one_mul, pow_lt_pow_right₀ hpos hi]
