no goals
𝕜 : Type ?u.44392
E : Type u_1
α : Type ?u.44398
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x * x⋆ = 0 ↔ x = 0
simpa only [star_eq_zero, star_star] using @star_mul_self_eq_zero_iff _ _ _ _ (star x)