Zulip Chat Archive
Stream: Is there code for X?
Topic: triangle equality if arg is equal
Eric Rodriguez (Mar 15 2022 at 14:01):
Do we have that (z + w).abs = z.abs + w.abs iff z.arg = w.arg? (possibly excluding zero)
Yaël Dillies (Mar 15 2022 at 14:12):
See #11794
Yaël Dillies (Mar 15 2022 at 14:13):
You'll need some glue to relate same_ray and complex.arg.
Eric Rodriguez (Mar 15 2022 at 14:28):
oh, nice! I'm no expert on this stuff but I was scrolling through and literally that condition is there
Eric Rodriguez (Mar 15 2022 at 14:32):
always nice when stuff works out this way^^
Alex J. Best (Mar 15 2022 at 14:55):
Are you thinking of using this for the cyclotomic PR @Eric Rodriguez . It would be quite useful there!
Yaël Dillies (Mar 15 2022 at 14:59):
A good deal of #11794 is ready already but I gathered that @Yury G. Kudryashov wanted to add some material.
Eric Rodriguez (Mar 15 2022 at 14:59):
precisely @Alex J. Best :)
Yaël Dillies (Mar 15 2022 at 15:10):
I'm always surprised when my stuff turns out useful :sweat_smile:
Time to get back to obscure order theory stuff, I guess.
Yury G. Kudryashov (Mar 16 2022 at 05:21):
You can prove that an inner product space is strictly convex first ;)
Yury G. Kudryashov (Mar 17 2022 at 23:38):
Done in #12790
Eric Rodriguez (Mar 17 2022 at 23:40):
nice! I also made #12764 so this should be all the glue necessary
Yury G. Kudryashov (Mar 17 2022 at 23:43):
I think that we should wait for #11794 and #12790, then update some statements in #12764 from implications to iffs.
Last updated: Dec 20 2023 at 11:08 UTC