Derivative of the inner product #
In this file we prove that the inner product and square of the norm in an inner space are
ℝ-smooth. In order to state these results, we need a
normed_space ℝ E
instance. Though we can deduce this structure from
inner_product_space 𝕜 E, this instance may be
not definitionally equal to some other “natural” instance. So, we assume
[normed_space ℝ E].