# Documentation

## Mathlib.Analysis.Complex.UnitDisc.Basic

In this file we define Complex.UnitDisc to be the unit disc in the complex plane. We also introduce some basic operations on this disc.

Complex unit disc.

Equations
Instances For

Complex unit disc.

Equations
Instances For
Equations
theorem Complex.UnitDisc.abs_lt_one (z : Complex.UnitDisc) :
Complex.abs â†‘z < 1
theorem Complex.UnitDisc.abs_ne_one (z : Complex.UnitDisc) :
Complex.abs â†‘z â‰  1
theorem Complex.UnitDisc.normSq_lt_one (z : Complex.UnitDisc) :
Complex.normSq â†‘z < 1
@[simp]
theorem Complex.UnitDisc.coe_mul (z : Complex.UnitDisc) (w : Complex.UnitDisc) :
â†‘(z * w) = â†‘z * â†‘w
def Complex.UnitDisc.mk (z : â„‚) (hz : Complex.abs z < 1) :

A constructor that assumes abs z < 1 instead of dist z 0 < 1 and returns an element of đť”» instead of â†ĄMetric.ball (0 : â„‚) 1.

Equations
Instances For
@[simp]
theorem Complex.UnitDisc.coe_mk (z : â„‚) (hz : Complex.abs z < 1) :
â†‘() = z
@[simp]
theorem Complex.UnitDisc.mk_coe (z : Complex.UnitDisc) (hz : optParam (Complex.abs â†‘z < 1) â‹Ż) :
Complex.UnitDisc.mk (â†‘z) hz = z
@[simp]
theorem Complex.UnitDisc.mk_neg (z : â„‚) (hz : Complex.abs (-z) < 1) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Complex.UnitDisc.coe_zero :
â†‘0 = 0
@[simp]
Equations
Equations
@[simp]
theorem Complex.UnitDisc.coe_smul_circle (z : â†Ącircle) (w : Complex.UnitDisc) :
â†‘(z â€˘ w) = â†‘z * â†‘w
Equations
@[simp]
theorem Complex.UnitDisc.coe_smul_closedBall (z : â†‘()) (w : Complex.UnitDisc) :
â†‘(z â€˘ w) = â†‘z * â†‘w

Real part of a point of the unit disc.

Equations
• z.re = (â†‘z).re
Instances For

Imaginary part of a point of the unit disc.

Equations
• z.im = (â†‘z).im
Instances For
@[simp]
theorem Complex.UnitDisc.re_coe (z : Complex.UnitDisc) :
(â†‘z).re = z.re
@[simp]
theorem Complex.UnitDisc.im_coe (z : Complex.UnitDisc) :
(â†‘z).im = z.im
@[simp]
theorem Complex.UnitDisc.re_neg (z : Complex.UnitDisc) :
(-z).re = -z.re
@[simp]
theorem Complex.UnitDisc.im_neg (z : Complex.UnitDisc) :
(-z).im = -z.im

Conjugate point of the unit disc.

Equations
Instances For
@[simp]
theorem Complex.UnitDisc.coe_conj (z : Complex.UnitDisc) :
â†‘z.conj = â†‘z
@[simp]
theorem Complex.UnitDisc.conj_conj (z : Complex.UnitDisc) :
z.conj.conj = z
@[simp]
theorem Complex.UnitDisc.conj_neg (z : Complex.UnitDisc) :
(-z).conj = -z.conj
@[simp]
theorem Complex.UnitDisc.re_conj (z : Complex.UnitDisc) :
z.conj.re = z.re
@[simp]
theorem Complex.UnitDisc.im_conj (z : Complex.UnitDisc) :
z.conj.im = -z.im
@[simp]
theorem Complex.UnitDisc.conj_mul (z : Complex.UnitDisc) (w : Complex.UnitDisc) :
(z * w).conj = z.conj * w.conj