`BookProof.ChapterSolidHarmonicTools.sum_inner_sq` (e : E) : ∑ i, (⟪e, (stdOrthonormalBasis ℝ E) i⟫_ℝ) ^ 2 = ‖e‖ ^ 2

Initializing...

`BookProof.ChapterSolidHarmonicTools.sum_inner_sq` (e : E) : ∑ i, (⟪e, (stdOrthonormalBasis ℝ E) i⟫_ℝ) ^ 2 = ‖e‖ ^ 2 · Prove2Me