Zulip Chat Archive

Stream: new members

Topic: (a/b).im = 0


Anders Larsson (Jan 04 2022 at 21:37):

Hi,
I I'm stuck on more complex math. If a and b (b <> 0) are real then obviously a/b is real. But do I prove it
if a and b are "declaired" complex?

import data.complex.basic
import tactic

open complex
open_locale complex_conjugate


lemma h (a b: ) (hai: a.im = 0) (hbi: b.im=0) (hnzb: b  0): (a / b).im = 0 :=
begin
  sorry,
end

Henrik Böving (Jan 04 2022 at 21:39):

I've never done proofs about complex numbers in Lean but my best guess would be that there is either a lemma that helps you here ooor you can unfold the definition of a/b and see what happens

Eric Rodriguez (Jan 04 2022 at 21:40):

simp [complex.div_im, hai, hbi]

Eric Rodriguez (Jan 04 2022 at 21:41):

you don't even need hnzb

Anders Larsson (Jan 04 2022 at 21:43):

Awesome! Thanx.


Last updated: Dec 20 2023 at 11:08 UTC