Zulip Chat Archive

Stream: new members

Topic: neg_eq_zero for complex numbers?


view this post on Zulip Răzvan Flavius Panda (Jan 10 2021 at 02:02):

z_rez_im: 
h: ¬{re := z_re, im := z_im} = 0
 0 < z_re ^ 2 + z_im ^ 2

I'm stuck on this goal and not sure how to make progress since neg_eq_zero is not working

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 02:02):

Do you know the maths proof?

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 02:04):

neg_eq_zero says x=0    x=0-x=0\implies x=0. I'm not sure what it has to do with this.

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 02:05):

- is negative, not logical "not".

view this post on Zulip Kevin Buzzard (Jan 10 2021 at 02:24):

[discussion moved elsewhere]


Last updated: May 10 2021 at 17:39 UTC