In this file we prove some basic lemmas about exp_map_circle and the restriction of complex.arg
to the unit circle. These two maps define a local equivalence between circle and ℝ, see
circle.arg_local_equiv and circle.arg_equiv, that sends the whole circle to (-π, π].
complex.arg ∘ coe and exp_map_circle define a local equivalence between circle andℝwithsource = set.univandtarget = set.Ioc (-π) π`.
complex.arg ∘ coe
complex.arg and exp_map_circle define an equivalence between circle and(-π, π]`.
exp_map_circle, applied to a real.angle.