Valuation of an algebraic element

The valuation of an element x algebraic over a field K is an n-th root of the valuation of some element of K, for some positive integer n at most the degree of x over K.

theorem Valuation.exists_map_pow_eq_map_algebraMap_of_isAlgebraic {K : Type u_1} {A : Type u_2} {Γ : Type u_3} [Field K] [Ring A] [Algebra K A] [LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ) {x : A} (hx : IsAlgebraic K x) : ∃ (n : ℕ) (r : K), 0 < n ∧ n ≤ (minpoly K x).natDegree ∧ v x ^ n = v ((algebraMap K A) r)

If x is algebraic over K, then v x is an n-th root of some v (algebraMap K A r).