(a/b).im = 0

Stream: new members

[Anders Larsson]

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]

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]

simp [complex.div_im, hai, hbi]

[Eric Rodriguez]

you don't even need hnzb

[Anders Larsson]

Awesome! Thanx.