Commit 2020-06-27 03:21 8413b3f4

feat(analysis/normed_space/real_inner_product): sums and bilinear form (#3187) Add lemmas about distributing the inner product into a sum. The natural approach to proving those seems to be to use the corresponding lemmas for bilinear forms, so also add a construction of a bilin_form ℝ α from the inner product. I realise this might all get refactored later if inner products get refactored to cover the case of complex inner products as well.