Hopf problem: uniformization · special periods 8

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

theorem Mathoverflow1973.SpecialPeriods.Triangle.trans_symm_exp_apply_mo1973_23439 {x y : ℂ} (a b : Path x y) (c r : ℂ) (ha : ∀ (t : ↑unitInterval), a t = c + r * Complex.exp (↑Real.pi * Complex.I * ↑↑t)) (hb : ∀ (t : ↑unitInterval), b t = c + r * Complex.exp (-(↑Real.pi * Complex.I * ↑↑t))) (t : ↑unitInterval) : (a.trans b.symm) t = c + r * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑t)