chore(analysis/normed_space/inner_product): euclidean space is a real inner product space

[urkud]

---

[eric-wieser]

Can you expand on the motivation for this? I'm worried that this introduces a diamond:

example {ι : Type*} [fintype ι] (f : ι → Type*)
  [Π i, inner_product_space ℝ (f i)] [Π i, inner_product_space 𝕜 (f i)] :
  (pi_Lp.inner_product_space f : inner_product_space ℝ (pi_Lp 2 f)) =
    @pi_Lp.inner_product_space_real 𝕜 _ _ _ _ _ := rfl  -- times out

which would be consistent with this comment saying the instances causes problems when 𝕜 = ℝ:

mathlib/src/analysis/inner_product_space/basic.lean

Lines 2098 to 2101 in 0c0dadf

	/-- A general inner product space structure implies a real inner product structure. This is not
	registered as an instance since it creates problems with the case `𝕜 = ℝ`, but in can be used in a
	proof to obtain a real inner product space structure from a given `𝕜`-inner product space
	structure. -/

[eric-wieser]

Oh, I guess [Π i, inner_product_space ℝ (f i)] [Π i, inner_product_space 𝕜 (f i)] is illegal because it puts two different additive group structures on f i...

[urkud]

I don't remember why I wanted this. I remember that I didn't use these instances in the final version, then abandoned this pr. We can close it if it leads to diamonds.