deduce `a = 0` from `a = -I*a`

Stream: new members

[Nicholas Wilson]

I'm trying to show that a function that satisfies the below relationships has a root at ± I:

example  (f : ℂ → ℂ)
         (f_one_div : f z = (1/z) * f z)
         (f_neg : f z = f (-z)) : f I = 0 := by
   let a := f I
   have one_div : f I = (1/I) * f (1/I) := by sorry --why does `rw [f_one_div]` or `rw [f_one_div I]` not work here???
   have neg : f (-I) = f (I) := by sorry -- ditto
   have neg_ab (a b :ℂ ) : -(a*b) = (-a)*b := by ring_nf
   conv_lhs =>
      rw [one_div]
      simp
      rw [neg_ab]
      rw [neg]
       -- here state is `⊢ -I* f I = 0`
   -- rough rest of logic is
   -- `1 * a = -I * a → (a = 0) ∨ (1 = -I)`
   -- `(a = 0) ∨ false`
   -- `a = 0`
   sorry

Silly question: why does rw [f_one_div] etc not work? it seems to work when it is a theorem (for a specific f).
Actual question: how do I show a = 0 following the sketch of the commented out proof above?

[Yongyi Chen]

You need to change f_one_div to ∀ z, f z = (1/z) * f z and similar for f_neg.