no goals
𝕜 : Type u_1
E : Type ?u.540761
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ normSq x = 0 ↔ inner x x = 0
simp only [normSq, ext_iff, map_zero, inner_self_im, eq_self_iff_true, and_true_iff]