Normed space over an RCLike field is a real normed space

Stream: Is there code for X?

[Michael Rothgang]

In Lean code, I'd like to prove this

import Mathlib
instance {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]: NormedSpace ℝ E := sorry

Intuitively, if k is the reals, we have nothing to prove --- and otherwise, k is a degree two extension of R. I don't know this corner of mathlib very well yet. If mathlib has this, what are the right terms to search for? Pointers to docs are fine answers, I'm happy to just read the manual :-)

[Michael Rothgang]

To un-#xy: proving this seems required for #23658, where we'd like to treat a complex manifold as a real manifold also. To state the property I want, I need to consider "such a manifold" (namely, a manifold over a model with corners on an RCLIke k) as a real manifold.

[Aaron Liu]

Probably docs#NormedSpace.restrictScalars

[Michael Rothgang]

:bulb: Ah right, that's the right terminology. Thanks!

[Anatole Dedecker]

In general we discourage using this to build an instance (although of course it can be useful in the middle of proofs) because it can create conflicting actions by the reals.

[Anatole Dedecker]

But this is explained in the docstring so I guess you knew already