Zulip Chat Archive
Stream: Is there code for X?
Topic: rat-normed space
Yaël Dillies (Apr 13 2022 at 13:11):
We have docs#normed_space.complex_to_real which turns normed_space ℂ E into normed_space ℝ E. Do we have something similar to turn normed_space ℝ E into normed_space ℚ E?
Yaël Dillies (Apr 13 2022 at 13:11):
Context is #13379
Eric Wieser (Apr 13 2022 at 13:13):
docs#normed_algebra_rat is all we have right now
Eric Wieser (Apr 13 2022 at 13:14):
Good luck avoiding a diamond
Yaël Dillies (Apr 13 2022 at 13:15):
What diamond is there to create? normed_space ℚ ℝ?
Eric Wieser (Apr 13 2022 at 13:17):
When E is a char_zero division ring
Yaël Dillies (Apr 13 2022 at 13:17):
Is it true more generally that normed_algebra 𝕜₁ 𝕜₂ → normed_space 𝕜₂ E → normed_space 𝕜₁ E?
Eric Wieser (Apr 13 2022 at 13:18):
Sure, that's probably docs#restrict_scalars.normed_space
Last updated: Dec 20 2023 at 11:08 UTC