complex negation

Stream: new members

[Răzvan Flavius Panda]

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]

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

[Ruben Van de Velde]

One option:

import data.complex.basic

example (z_re z_im: ℝ) (h2: z_re = 0) (h: ¬({re := 0, im := z_im} : ℂ) = 0) : 0 < z_re ^ 2 + z_im ^ 2 :=
begin
  rw [h2, zero_pow zero_lt_two, zero_add],
  apply lt_of_le_of_ne (pow_two_nonneg _),
  contrapose! h,
  obtain rfl := pow_eq_zero h.symm,
  refl,
end

[Răzvan Flavius Panda]

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

[Kevin Buzzard]

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]

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

[Răzvan Flavius Panda]

@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]

this negates a proposition not a complex number

[Răzvan Flavius Panda]

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