∀ {R : Type u_2} {Γ₀ : Type u_3} {Γ'₀ : Type u_1} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] (f : Γ₀ →*₀ Γ'₀) (v : Valuation R Γ₀),
  (↑(f.comp v.toMonoidWithZeroHom)).toFun 0 = 0