mathlib documentation

analysis.complex.unit_disc.basic

Poincaré disc #

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp, norm_cast]

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
@[simp]
theorem complex.unit_disc.coe_mk (z : ) (hz : complex.abs z < 1) :
@[protected, instance]
Equations
@[simp]
@[simp]
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]

Real part of a point of the unit disc.

Equations

Imaginary part of a point of the unit disc.

Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]

Conjugate point of the unit disc.

Equations
@[simp]
@[simp]