𝕜 : Type u_2
inst✝² : IsROrC 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
have : ‖x‖ ≠ 0 := by simp [hx]
no goals
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
field_simp [norm_smul]
no goals
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0
simp [hx]