Hopf problem: elliptic · core 2

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.Elliptic.complexPower_isLocalDiffeomorphAt (m : ℕ) (hm : 0 < m) (z : ℂ) (hz : z ≠ 0) : IsLocalDiffeomorphAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (fun (w : ℂ) => w ^ m) z