mathlib3 documentation

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

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) :

complex.argcoe and exp_map_circle define a local equivalence between circle andwithsource = set.univandtarget = set.Ioc (-π) π`.


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

theorem real.angle.exp_map_circle_add (θ₁ θ₂ : real.angle) :
(θ₁ + θ₂).exp_map_circle = θ₁.exp_map_circle * θ₂.exp_map_circle