# mathlib3documentation

analysis.special_functions.complex.circle

# Maps on the unit circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (-π, π].

@[simp]
theorem circle.arg_eq_arg {z w : circle} :
z.arg = w.arg z = w
theorem arg_exp_map_circle {x : } (h₁ : -real.pi < x) (h₂ : x real.pi) :
@[simp]
theorem exp_map_circle_arg (z : circle) :
@[simp]
@[simp]
noncomputable def circle.arg_local_equiv  :

complex.arg ∘ coe and exp_map_circle define a local equivalence between circle andwithsource = set.univandtarget = set.Ioc (-π) π.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def circle.arg_equiv  :

complex.arg and exp_map_circle define an equivalence between circle and(-π, π].

Equations
theorem exp_map_circle_eq_exp_map_circle {x y : } :
(m : ), x = y + m * (2 * real.pi)
@[simp]
theorem exp_map_circle_two_pi  :
= 1
noncomputable def real.angle.exp_map_circle (θ : real.angle) :

exp_map_circle, applied to a real.angle.

Equations
@[simp]
@[simp]
theorem real.angle.exp_map_circle_add (θ₁ θ₂ : real.angle) :
(θ₁ + θ₂).exp_map_circle =