Covering maps involving the complex plane

In this file, we show that Complex.exp is a covering map on {0}ᶜ.

theorem Complex.isAddQuotientCoveringMap_exp : IsAddQuotientCoveringMap (fun (z : ℂ) => ⟨exp z, ⋯⟩) ↥(AddSubgroup.zmultiples (2 * ↑Real.pi * I))

theorem Complex.isCoveringMap_exp : IsCoveringMap fun (z : ℂ) => ⟨exp z, ⋯⟩

exp : ℂ → ℂ \ {0} is a covering map.

theorem Complex.isCoveringMapOn_exp : IsCoveringMapOn exp {0}ᶜ

theorem Polynomial.isCoveringMapOn_eval {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (p : Polynomial 𝕜) : IsCoveringMapOn (fun (x : 𝕜) => eval x p) ((fun (x : 𝕜) => eval x p) '' {k : 𝕜 | eval k (derivative p) = 0})ᶜ