Real part of the complex winding normalization

Multiplication by (2πi)⁻¹ converts an imaginary part into the real normalized index.

theorem Complex.re_inv_two_pi_I_mul (w : ℂ) : ((2 * ↑Real.pi * I)⁻¹ * w).re = w.im / (2 * Real.pi)

The real part of a normalized complex winding integral is its imaginary part divided by 2π.