Commit 2020-06-14 16:36 1f16da1b

refactor(analysis/normed_space/real_inner_product): extend normed_space in the definition (#3060) Currently, inner product spaces do not extend normed spaces, and a norm is constructed from the inner product. This makes it impossible to put an instance on reals, because it would lead to two non-defeq norms. We refactor inner product spaces to extend normed spaces, with the condition that the norm is equal (but maybe not defeq) to the square root of the inner product, to solve this issue. The possibility to construct a norm from a well-behaved inner product is still given by a constructor inner_product_space.of_core. We also register the inner product structure on a finite product of inner product spaces (not on the Pi type, which has the sup norm, but on pi_Lp 2 one_le_two \alpha which has the right norm).