Stream: new members

Topic: complex negation

Răzvan Flavius Panda (Jan 10 2021 at 13:24):

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


what can be used to rw ~ in h?

Kevin Buzzard (Jan 10 2021 at 13:38):

What do you want to rewrite it to? What are you trying to do mathematically?

One option:

Răzvan Flavius Panda (Jan 10 2021 at 14:04):

@Kevin Buzzard apply negation to both parts of the complex number then split h into 2 equialities maybe

Kevin Buzzard (Jan 10 2021 at 14:23):

You do understand that $\lnot$ doesn't mean $-$ right? Are you confusing logical negation $\lnot P$ with the negative of a number $-z$? I am still at a loss with this question. Can you write down in Lean what you want to rewrite the equation to?

Reid Barton (Jan 10 2021 at 14:27):

And in particular ¬{re := 0, im := z_im} = 0 means ¬ ({re := 0, im := z_im} = 0)

Răzvan Flavius Panda (Jan 10 2021 at 17:08):

@Kevin Buzzard yes, I understand, you told me that in Xena DIscord. so I'd like to apply ~ to that complex number
isn't negating a complex number negating both of its components?

Kenny Lau (Jan 10 2021 at 17:09):

this negates a proposition not a complex number

Răzvan Flavius Panda (Jan 10 2021 at 19:52):

Oh, so ~ is actually negating the entire proposition: {re := 0, im := z_im} = 0
only seen now what @Reid Barton said

Last updated: May 14 2021 at 13:24 UTC