`BookProof.ChapterCoherentOverlap.norm_sq_eq_sum` (q : EuclideanSpace ℝ (Fin n)) : ‖q‖ ^ 2 = ∑ i, q i * q i

Initializing...

`BookProof.ChapterCoherentOverlap.norm_sq_eq_sum` (q : EuclideanSpace ℝ (Fin n)) : ‖q‖ ^ 2 = ∑ i, q i * q i · Prove2Me