∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {P : Type u_3} {S : Type u_4}
  [inst_1 : Ring R] [inst_2 : SMul P S] [inst_3 : SMul S R] [inst_4 : SMul P R] [IsScalarTower P S R]
  (v : Valuation R Γ₀), IsScalarTower P S (WithVal v)