Hilbert spaces induces a real smul

Stream: mathlib4

[Alex Meiburg]

The following doesn't work atm:

import Mathlib

--E is a HilbertSpace over 𝕜
variable (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]

example (x : E) : (3 : ℕ) • x = (3 : 𝕜) • x := by
  rw [ofNat_smul_eq_nsmul 𝕜 3 x]

example (x : E) : (3 : ℕ) • x = (3 : ℚ) • x := by --error
  sorry

example (x : E) : (3 : ℕ) • x = (3 : ℝ) • x := by --eror
  sorry

That is, the 𝕜-smul works, but there is no ℚ-smul or ℝ-smul. You can write (↑(3 : ℚ) : 𝕜) • x and (↑(3 : ℝ) : 𝕜) • x instead. In my view the rat-smul and real-smul are "natural" enough that we could offer these SMul instances. Before I write this PR, is there a reason it would be bad?

[Alex Meiburg]

^^ I guess the above is slightly un-minimal, we really only need SeminormedAddCommGroup and there's no need for the CompleteSpace.

[Jireh Loreaux]

Yes, this would be bad. Think of what happens when E is \R or \C itself.

[Alex Meiburg]

Oh, right. Hrmg, that's unfortunate.

[Alex Meiburg]

And if they are, the RCLike instance won't give something defeq? If it _was_ defeq it would work, maybe, right?

[Jireh Loreaux]

If you need it in a proof, just use RestrictScalars and if you need it in a statement, assume you have the relevant \R instance and add IsScalarTower.

[Aaron Liu]

I think the "correct" way to do this is to write [Module ℚ E] [IsScalarTower ℚ 𝕜 E] or something similar

[Jireh Loreaux]

(but you only need to do that if you need it for the statement to compile.)

[Alex Meiburg]

Ahh I see. Makes sense now, yeah. But man, these things about RCLike remain unintuitive for me!