valuation_monomial_eq_valuation_X_pow

English

If a valuation v on RatFunc(K) is trivial on constants, then for every natural n and every nonzero a ∈ K, the monomial n-th degree has valuation v(monomial n a) = v(X)^n.

Русский

Если на вычислении v на RatFunc(K) тривиальна на константах, то для любого натурального n и любого ненулевого a ∈ K выполняется v(monomial n a) = v(X)^n.

LaTeX

$$$\forall n\in\mathbb{N}, \forall a\in K\setminus\{0\},\quad v(\operatorname{monomial} n\ a) = v(\mathrm{X})^{n}$$$

Lean4

/-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of
`(monomial n a)` is equal to `(v RatFunc.X) ^ n`. -/
theorem valuation_monomial_eq_valuation_X_pow (n : ℕ) {a : K} (ha : a ≠ 0) : v (monomial n a) = v RatFunc.X ^ n := by
  simp_all [RatFunc.coePolynomial, ← C_mul_X_pow_eq_monomial]

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