Hopf problem: uniformization · cusp uniformization 3

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

noncomputable def Mathoverflow1973.CuspUniformization.localLog (z0 z : ℂ) : ℂ

A branch of the normalized logarithm centered at a nonzero point.

Equations

• Mathoverflow1973.CuspUniformization.localLog z0 z = Mathoverflow1973.CuspUniformization.logarithm z0 + Mathoverflow1973.CuspUniformization.logarithm (z / z0)

theorem Mathoverflow1973.CuspUniformization.logarithm_eq_localLog_add_int {z0 z : ℂ} (hz0 : z0 ≠ 0) (hz : z ≠ 0) : ∃ (n : ℤ), logarithm z = localLog z0 z + ↑n