Commit 2020-06-27 03:21 8413b3f4
View on Github →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.