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