mathlib3

8413b3f4 - feat(analysis/normed_space/real_inner_product): sums and bilinear form (#3187)

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.