# mathlib3documentation

analysis.complex.unit_disc.basic

# Poincaré disc #

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

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]
noncomputable def complex.unit_disc.topological_space  :
@[protected, instance]

Complex unit disc.

Equations
Instances for complex.unit_disc
@[protected, instance]
noncomputable def complex.unit_disc.has_distrib_neg  :
@[protected, instance]
noncomputable def complex.unit_disc.comm_semigroup  :
@[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 : < 1) :
hz) = z
@[simp]
theorem complex.unit_disc.mk_coe (z : complex.unit_disc) (hz : := _) :
= z
@[simp]
theorem complex.unit_disc.mk_neg (z : ) (hz : < 1) :
hz =
@[protected, instance]
Equations
@[simp]
@[simp]
@[protected, instance]
noncomputable def complex.unit_disc.inhabited  :
Equations
@[protected, instance]
noncomputable def complex.unit_disc.circle_action  :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp, norm_cast]
@[protected, instance]
noncomputable def complex.unit_disc.closed_ball_action  :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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, norm_cast]
@[simp]
@[simp]