feat(data/complex/is_R_or_C): register some instances (#5466)
Register a couple of facts which were previously known for `ℝ` and `ℂ` individually, but not for the typeclass `[is_R_or_C K]`:
- such a field `K` is finite-dimensional as a vector space over `ℝ`
- finite-dimensional normed spaces over `K` are proper.
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Instances.20for.20is_R_or_C
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
