`BookProof.ChapterCoherentOverlap.norm_sub_sq_expand` (q k : EuclideanSpace ℝ (Fin n)) : ‖q - k‖ ^ 2 = ‖q‖ ^ 2 + ‖k‖ ^ 2

Initializing...

`BookProof.ChapterCoherentOverlap.norm_sub_sq_expand` (q k : EuclideanSpace ℝ (Fin n)) : ‖q - k‖ ^ 2 = ‖q‖ ^ 2 + ‖k‖ ^ 2 - 2 * inner ℝ q k · Prove2Me