∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
  [inst_4 : ValuationRing A] [inst_5 : IsFractionRing A K],
  (ValuationRing.valuation A K).integer = (algebraMap A K).range