Zulip Chat Archive
Stream: Is there code for X?
Topic: normed space real of complex
Yury G. Kudryashov (Sep 21 2021 at 01:51):
Do we have an instance for [normed_space complex E] : normed_space real E? I failed to quickly find it.
Eric Wieser (Sep 21 2021 at 05:47):
I expect it's a def
Eric Wieser (Sep 21 2021 at 05:47):
Or a type alias
Eric Wieser (Sep 21 2021 at 05:48):
docs#restrict_scalars.normed_space
Eric Wieser (Sep 21 2021 at 05:48):
docs#normed_space.restrict_scalars
Eric Wieser (Sep 21 2021 at 05:49):
Evidently we have both an alias and a def
Sebastien Gouezel (Sep 21 2021 at 06:45):
Still, it should probably be registered as a global instance. For instance, the fact that a complex module is also a real module is registered as a global instance (and is used heavily). I have just checked, and indeed it is not registered yet for normed spaces.
Eric Wieser (Sep 21 2021 at 07:00):
What's the module instance you're referring to?
Sebastien Gouezel (Sep 21 2021 at 07:20):
Yury G. Kudryashov (Sep 23 2021 at 02:12):
Added docs#complex.normed_space in #9326 (already merged; should be renamed to normed_space.complex_to_real).
Eric Wieser (Sep 24 2021 at 13:41):
Renamed in #9366
Last updated: Dec 20 2023 at 11:08 UTC