Zulip Chat Archive

Stream: new members

Topic: complex negation


view this post on Zulip 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?

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

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

view this post on Zulip Ruben Van de Velde (Jan 10 2021 at 13:59):

One option:

view this post on Zulip 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

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

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

view this post on Zulip Reid Barton (Jan 10 2021 at 14:27):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jan 10 2021 at 17:09):

this negates a proposition not a complex number

view this post on Zulip 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