feat(analysis/inner_product_space/basic): inner products of linear combinations of orthonormal vectors (#11323)
There are some lemmas about the inner product of a linear combination
of orthonormal vectors with one vector from that orthonormal family.
Add similar lemmas where both sides of the inner product are linear
combinations.