𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑re ↑(normSq x) = ↑re (inner x x) ∧ ↑im ↑(normSq x) = ↑im (inner x x)
𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑(normSq x) = inner x x
rw [ext_iff]
no goals
𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑re ↑(normSq x) = ↑re (inner x x) ∧ ↑im ↑(normSq x) = ↑im (inner x x)
exact ⟨by simp only [ofReal_re]; rfl, by simp only [inner_self_im, ofReal_im]⟩
𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ normSq x = ↑re (inner x x)
𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑re ↑(normSq x) = ↑re (inner x x)
simp only [ofReal_re]
no goals
𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ normSq x = ↑re (inner x x)
rfl
no goals
𝕜 : Type u_1
E : Type ?u.365837
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑im ↑(normSq x) = ↑im (inner x x)
simp only [inner_self_im, ofReal_im]