The angle between I and I * w

The unoriented angle between I and I * w is arccos (Re w / |w|) (Complex.angle_I_I_mul); for w in the open upper half-plane this is the argument of w.

Main results

• Complex.angle_I_I_mul: angle I (I * w) = arccos (w.re / ‖w‖).

theorem Complex.angle_I_I_mul (w : ℂ) : InnerProductGeometry.angle I (I * w) = Real.arccos (w.re / ‖w‖)

The angle between I and I * w is arccos (Re w / |w|); for w in the upper half-plane this is the argument of w.