Commit 2022-07-26 11:31 b21c9aa1
View on Github →chore(analysis/inner_product_space): golf two proofs (#15679)
Golf two proofs and move the lemmas into inner_product_space/basic since they now only depend on elementary facts about inner product spaces.