# The circle #

This file defines circle to be the metric sphere (Metric.sphere) in ℂ centred at 0 of radius 1. We equip it with the following structure:

• a submonoid of ℂ
• a group
• a topological group

We furthermore define expMapCircle to be the natural map fun t ↦ exp (t * I) from ℝ to circle, and show that this map is a group homomorphism.

## Implementation notes #

Because later (in Geometry.Manifold.Instances.Sphere) one wants to equip the circle with a smooth manifold structure borrowed from Metric.sphere, the underlying set is {z : ℂ | abs (z - 0) = 1}. This prevents certain algebraic facts from working definitionally -- for example, the circle is not defeq to {z : ℂ | abs z = 1}, which is the kernel of Complex.abs considered as a homomorphism from ℂ to ℝ, nor is it defeq to {z : ℂ | normSq z = 1}, which is the kernel of the homomorphism Complex.normSq from ℂ to ℝ.

@[deprecated]
def circle :

The unit circle in ℂ, here given the structure of a submonoid of ℂ.

Please use Circle when referring to the circle as a type.

Equations
Instances For
@[deprecated]
theorem mem_circle_iff_abs {z : } :
Complex.abs z = 1
@[deprecated]
theorem mem_circle_iff_normSq {z : } :
Complex.normSq z = 1

The unit circle in ℂ.

Equations
Instances For
Equations
Equations
Equations
theorem Circle.ext_iff {x : Circle} {y : Circle} :
x = y x = y
theorem Circle.ext {x : Circle} {y : Circle} :
x = yx = y
theorem Circle.coe_inj {x : Circle} {y : Circle} :
x = y x = y
@[simp]
theorem Circle.abs_coe (z : Circle) :
Complex.abs z = 1
@[simp]
theorem Circle.normSq_coe (z : Circle) :
Complex.normSq z = 1
@[simp]
theorem Circle.coe_ne_zero (z : Circle) :
z 0
@[simp]
theorem Circle.coe_one :
1 = 1
theorem Circle.coe_eq_one {x : Circle} :
x = 1 x = 1
@[simp]
theorem Circle.coe_mul (z : Circle) (w : Circle) :
(z * w) = z * w
@[simp]
theorem Circle.coe_inv (z : Circle) :
z⁻¹ = (↑z)⁻¹
theorem Circle.coe_inv_eq_conj (z : Circle) :
z⁻¹ = z
@[simp]
theorem Circle.coe_div (z : Circle) (w : Circle) :
(z / w) = z / w
@[simp]
theorem Circle.coeHom_apply (self : { x : // }) :
Circle.coeHom self = self

The coercion Circle → ℂ as a monoid homomorphism.

Equations
Instances For
@[deprecated Circle.abs_coe]
theorem abs_coe_circle (z : Circle) :
Complex.abs z = 1

Alias of Circle.abs_coe.

@[deprecated Circle.normSq_coe]
theorem normSq_eq_of_mem_circle (z : Circle) :
Complex.normSq z = 1

Alias of Circle.normSq_coe.

@[deprecated Circle.coe_ne_zero]
theorem ne_zero_of_mem_circle (z : Circle) :
z 0

Alias of Circle.coe_ne_zero.

@[deprecated Circle.coe_inv]
theorem coe_inv_circle (z : Circle) :
z⁻¹ = (↑z)⁻¹

Alias of Circle.coe_inv.

@[deprecated Circle.coe_inv_eq_conj]
theorem coe_inv_circle_eq_conj (z : Circle) :
z⁻¹ = z

Alias of Circle.coe_inv_eq_conj.

@[deprecated Circle.coe_div]
theorem coe_div_circle (z : Circle) (w : Circle) :
(z / w) = z / w

Alias of Circle.coe_div.

The elements of the circle embed into the units.

Equations
Instances For
@[simp]
theorem Circle.toUnits_apply (z : Circle) :
Circle.toUnits z = Units.mk0 z
Equations
Equations
Equations
Equations
@[simp]
theorem Circle.ofConjDivSelf_coe (z : ) (hz : z 0) :
(Circle.ofConjDivSelf z hz) = z / z
def Circle.ofConjDivSelf (z : ) (hz : z 0) :

If z is a nonzero complex number, then conj z / z belongs to the unit circle.

Equations
• = z / z,
Instances For

The map fun t => exp (t * I) from ℝ to the unit circle in ℂ.

Equations
Instances For
@[simp]
theorem Circle.coe_exp (t : ) :
(Circle.exp t) = Complex.exp (t * Complex.I)
@[simp]
theorem Circle.exp_zero :
Circle.exp 0 = 1
@[simp]
theorem Circle.exp_add (x : ) (y : ) :
Circle.exp (x + y) = Circle.exp x * Circle.exp y
@[simp]
theorem Circle.expHom_apply :
∀ (a : ), Circle.expHom a = (Additive.ofMul ) a

The map fun t => exp (t * I) from ℝ to the unit circle in ℂ, considered as a homomorphism of groups.

Equations
Instances For
@[simp]
theorem Circle.exp_sub (x : ) (y : ) :
Circle.exp (x - y) = Circle.exp x / Circle.exp y
@[simp]
theorem Circle.exp_neg (x : ) :
Circle.exp (-x) = (Circle.exp x)⁻¹
instance Circle.instSMul {α : Type u_1} [] :
Equations
• Circle.instSMul = .smul
instance Circle.instSMulCommClass_left {α : Type u_1} {β : Type u_2} [] [SMul α β] [] :
Equations
• =
instance Circle.instSMulCommClass_right {α : Type u_1} {β : Type u_2} [] [SMul α β] [] :
Equations
• =
instance Circle.instIsScalarTower {α : Type u_1} {β : Type u_2} [] [] [SMul α β] [] :
Equations
• =
instance Circle.instMulAction {α : Type u_1} [] :
Equations
• Circle.instMulAction = .mulAction
instance Circle.instDistribMulAction {M : Type u_3} [] [] :
Equations
• Circle.instDistribMulAction = .distribMulAction
theorem Circle.smul_def {α : Type u_1} [] (z : Circle) (a : α) :
z a = z a
instance Circle.instContinuousSMul {α : Type u_1} [] [] [] :
Equations
• =
@[simp]
theorem Circle.norm_smul {E : Type u_4} [] (u : Circle) (v : E) :
@[deprecated Circle.exp]

Alias of Circle.exp.

The map fun t => exp (t * I) from ℝ to the unit circle in ℂ.

Equations
Instances For
@[deprecated Circle.coe_exp]
theorem expMapCircle_apply (t : ) :
(Circle.exp t) = Complex.exp (t * Complex.I)

Alias of Circle.coe_exp.

@[deprecated Circle.exp_zero]
theorem expMapCircle_zero :
Circle.exp 0 = 1

Alias of Circle.exp_zero.

@[deprecated Circle.exp_sub]
theorem expMapCircle_sub (x : ) (y : ) :
Circle.exp (x - y) = Circle.exp x / Circle.exp y

Alias of Circle.exp_sub.

@[deprecated Circle.norm_smul]
theorem norm_circle_smul {E : Type u_4} [] (u : Circle) (v : E) :

Alias of Circle.norm_smul.