𝕜 : Type ?u.40337
E : Type u_1
α : Type ?u.40343
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0
𝕜 : Type ?u.40337
E : Type u_1
α : Type ?u.40343
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0
rw [← norm_eq_zero, norm_star_mul_self]
no goals
𝕜 : Type ?u.40337
E : Type u_1
α : Type ?u.40343
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0
exact mul_self_eq_zero.trans norm_eq_zero