## Stream: new members

### Topic: neg_eq_zero for complex numbers?

#### 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

#### Kevin Buzzard (Jan 10 2021 at 02:02):

Do you know the maths proof?

#### Kevin Buzzard (Jan 10 2021 at 02:04):

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

#### Kevin Buzzard (Jan 10 2021 at 02:05):

$-$ is negative, not logical "not".

#### Kevin Buzzard (Jan 10 2021 at 02:24):

[discussion moved elsewhere]

Last updated: May 10 2021 at 17:39 UTC