𝕜 : Type u_2
E : Type u_3
F : Type ?u.2128451
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
em✝ : (a : Prop) → Decidable a
⊢ ∑ i in s, ∑ j in s, a i j • inner (v j) (v i) = ∑ k in s, a k k
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2128451
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
⊢ ∑ i in s, ∑ j in s, a i j • inner (v j) (v i) = ∑ k in s, a k k
classical!
no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2128451
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec_ι : DecidableEq ι
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
em✝ : (a : Prop) → Decidable a
⊢ ∑ i in s, ∑ j in s, a i j • inner (v j) (v i) = ∑ k in s, a k k
simp [orthonormal_iff_ite.mp hv, Finset.sum_ite_of_true]