valuation_inv_monomial_eq_valuation_X_zpow

English

For any n and nonzero a ∈ K, the valuation of 1/(monomial n a) equals v(X) raised to the power -(n) as an integer exponent: v(1/(monomial n a)) = v(X)^{-(n:ℤ)}.

Русский

Для любого n и ненулевого a ∈ K, оценка 1/(monomial n a) равна v(X)^{-(n)}, где показатель степени берётся как целое число: v(1/(monomial n a)) = v(X)^{-(n:ℤ)}.

LaTeX

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

Lean4

/-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of
`1 / (monomial n a)` (as an element of the field of rational functions) is equal
to `(v RatFunc.X) ^ (- n)`. -/
theorem valuation_inv_monomial_eq_valuation_X_zpow (n : ℕ) {a : K} (ha : a ≠ 0) :
    v (1 / monomial n a) = v RatFunc.X ^ (-(n : ℤ)) := by simpa using valuation_monomial_eq_valuation_X_pow _ hv n ha

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