no goals
K : Type ?u.1561683
F : Type ?u.1561686
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1561698
Γ''₀ : Type ?u.1561701
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x - y) = ↑v (x + -y)
rw [sub_eq_add_neg]
no goals
K : Type ?u.1561683
F : Type ?u.1561686
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1561698
Γ''₀ : Type ?u.1561701
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ max (↑v x) (↑v (-y)) = max (↑v x) (↑v y)
rw [map_neg]