Zulip Chat Archive
Stream: Is there code for X?
Topic: non-submultiplicative normed ring?
Monica Omar (Jul 21 2025 at 13:35):
Is there code for an inner product space that’s also an algebra, but not necessarily that ‖x * y‖ ≤ ‖x‖ * ‖y‖?
So docs#NormedRing but without the norm_mul_le property?
Eric Wieser (Jul 21 2025 at 13:46):
No, and I think probably the plan is to achieve this via changing the spelling of [NormedRing R] to [Ring R] [NormedRing R]
Eric Wieser (Jul 21 2025 at 13:46):
With that change, what you want would be [Ring R] [NormedAddCommGroup R]
Monica Omar (Jul 21 2025 at 13:48):
Eric Wieser said:
With that change, what you want would be
[Ring R] [NormedAddCommGroup R]
Yes, exactly this. But this would create non-defeq diamonds.
Yaël Dillies (Jul 21 2025 at 13:54):
Not if NormedAddCommGroup R doesn't extend AddCommGroup R
Monica Omar (Jul 21 2025 at 13:55):
Right. So is the plan to refactor NormedAddCommGroup?
Monica Omar (Jul 21 2025 at 13:58):
perhaps to take in AddCommGroup and extend Norm and MetricSpace?
Eric Wieser (Jul 21 2025 at 14:00):
Monica Omar said:
Right. So is the plan to refactor
NormedAddCommGroup?
More of a concept of a plan
Eric Wieser (Jul 21 2025 at 14:00):
#24040 implements this idea
Last updated: Dec 20 2025 at 21:32 UTC