Hopf problem: uniformization · special periods 7

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

theorem Mathoverflow1973.SpecialPeriods.Triangle.complex_eq_of_re_eq_norm_add_one_eq {z w : ℂ} (hr : z.re = w.re) (hz : 0 < z.im) (hw : 0 < w.im) (hn : ‖z + 1‖ = ‖w + 1‖) : z = w