The additive circle and the complex unit circle

For a nonzero real period T, Mathlib's AddCircle.homeomorphCircle identifies AddCircle T with the complex unit circle Circle. This file records where that identification sends the distinguished points: 0 : AddCircle T is the point 1 : Circle, so the inverse homeomorphism carries 1 back to 0.

Main results

• AddCircle.homeomorphCircle_symm_one — the inverse circle homeomorphism sends 1 to 0 for every nonzero real period.

@[simp]

theorem AddCircle.homeomorphCircle_symm_one {T : ℝ} (hT : T ≠ 0) : (homeomorphCircle hT).symm 1 = 0

The inverse homeomorphism AddCircle.homeomorphCircle.symm carries 1 : Circle to 0.