case a
𝕜 : Type u_1
𝕝 : Type ?u.117311
E : Type u_2
ι : Sort ?u.117317
κ : ι → Sort ?u.117322
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ (-x ∈ s ↔ x ∈ s) ↔ (-1 • x ∈ s ↔ 1 • x ∈ s)
𝕜 : Type u_1
𝕝 : Type ?u.117311
E : Type u_2
ι : Sort ?u.117317
κ : ι → Sort ?u.117322
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ -x ∈ s ↔ x ∈ s
convert hs.mem_smul_iff (x := x) (norm_neg 1) using 0
no goals
case a
𝕜 : Type u_1
𝕝 : Type ?u.117311
E : Type u_2
ι : Sort ?u.117317
κ : ι → Sort ?u.117322
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ (-x ∈ s ↔ x ∈ s) ↔ (-1 • x ∈ s ↔ 1 • x ∈ s)
simp only [neg_smul, one_smul 𝕜 x]