no goals
R : Type ?u.1254732
R' : Type ?u.1254735
𝕜 : Type u_2
𝕜₂ : Type ?u.1254741
𝕜₃ : Type ?u.1254744
𝕝 : Type ?u.1254747
E : Type u_1
E₂ : Type ?u.1254753
E₃ : Type ?u.1254756
F : Type ?u.1254759
G : Type ?u.1254762
ι : Type ?u.1254765
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
r : ℝ
hx : x ∈ ball p 0 r
⊢ ‖-1‖ ≤ 1
rw [norm_neg, norm_one]
no goals
R : Type ?u.1254732
R' : Type ?u.1254735
𝕜 : Type u_2
𝕜₂ : Type ?u.1254741
𝕜₃ : Type ?u.1254744
𝕝 : Type ?u.1254747
E : Type u_1
E₂ : Type ?u.1254753
E₃ : Type ?u.1254756
F : Type ?u.1254759
G : Type ?u.1254762
ι : Type ?u.1254765
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
r : ℝ
hx : x ∈ ball p 0 r
⊢ (fun x => -1 • x) x = -x
simp only [neg_smul, one_smul]