Mathlib

Atlas/Analysis/Complex analysis

Multiply by rotating

1/4

A complex number is a length and an angle from the positive real axis.