English
Let K be a field, L a K-algebra, Γ a linearly ordered commutative group with zero, and v a valuation on L that is trivial on K via algebra maps: v(algebraMap_K_L(a)) = 1 for all a ≠ 0 in K. Then for every w ∈ L, every n ∈ N, and every a ∈ K with a ≠ 0, we have v((monomial n a).aeval w) = (v w)^n.
Русский
Пусть K — поле, L — K-алгебра, Γ — линейно упорядоченная коммутативная группа с нулём, и v — оценка на L, тривиальная на константах через алгебраическое отображение: v(algebraMap_K_L(a)) = 1 при a ≠ 0. Тогда для каждого w ∈ L, каждого n ∈ ℕ и каждого a ∈ K, a ≠ 0, выполняется v((monomial n a).aeval w) = (v(w))^n.
LaTeX
$$$\forall w\in L, \forall n\in\mathbb{N}, \forall a\in K\setminus\{0\},\quad v\big((\operatorname{monomial} n\ a).\mathrm{aeval}\, w\big) = (v(w))^{n}$$$
Lean4
theorem valuation_aeval_monomial_eq_valuation_pow (w : L) (n : ℕ) {a : K} (ha : a ≠ 0) :
v ((monomial n a).aeval w) = (v w) ^ n := by simp [← C_mul_X_pow_eq_monomial, map_mul, map_pow, one_mul, hv a ha]
