Theorems · Theorem · field theory

Polynomial.valuation_inv_monomial_eq_valuation_X_zpow

∀ (K : Type u_1) [inst : Field K] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K},
  a ≠ 0 → v (1 / ↑((Polynomial.monomial n) a)) = v RatFunc.X ^ (-↑n)

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).

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

0 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderedCommGroupWithZeroValuation.IsTrivialOn