𝕜 : Type u_1
E : Type ?u.547403
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑re ↑(↑re (inner x x)) = ↑re (inner x x) ∧ ↑im ↑(↑re (inner x x)) = 0
𝕜 : Type u_1
E : Type ?u.547403
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑(↑re (inner x x)) = inner x x
rw [ext_iff, inner_self_im]
no goals
𝕜 : Type u_1
E : Type ?u.547403
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑re ↑(↑re (inner x x)) = ↑re (inner x x) ∧ ↑im ↑(↑re (inner x x)) = 0
norm_num