no goals
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (x + -y)
rw [sub_eq_add_neg]
no goals
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e x + ↑e (-y) = ↑e x + ↑e y
rw [e.map_neg]