∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {A : Type u_7}
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R],
  v₁.IsEquiv v₂ → (Valuation.IsTrivialOn A v₁ ↔ Valuation.IsTrivialOn A v₂)