∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : CommRing R]
  [inst_2 : ValuativeRel R] [MulArchimedean Γ₀] (v : Valuation R Γ₀) [v.Compatible], ValuativeRel.IsRankLeOne R