no goals
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ ↑e (-x) = ↑‖-1‖₊ * ↑e x
rw [← map_smul, neg_one_smul]
no goals
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ ↑‖-1‖₊ * ↑e x = ↑e x
simp