Documentation

Mathlib.Analysis.Complex.UnitDisc.Basic

PoincarΓ© disc #

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.

Instances For
    @[simp]
    theorem Complex.UnitDisc.coe_mul (z : Complex.UnitDisc) (w : Complex.UnitDisc) :
    ↑(z * w) = ↑z * ↑w

    A constructor that assumes abs z < 1 instead of dist z 0 < 1 and returns an element of 𝔻 instead of β†₯Metric.ball (0 : β„‚) 1.

    Instances For
      @[simp]
      theorem Complex.UnitDisc.coe_mk (z : β„‚) (hz : ↑Complex.abs z < 1) :
      ↑(Complex.UnitDisc.mk z hz) = z
      @[simp]
      theorem Complex.UnitDisc.mk_coe (z : Complex.UnitDisc) (hz : optParam (↑Complex.abs ↑z < 1) (_ : ↑Complex.abs ↑z < 1)) :
      Complex.UnitDisc.mk (↑z) hz = z
      @[simp]
      theorem Complex.UnitDisc.mk_neg (z : β„‚) (hz : ↑Complex.abs (-z) < 1) :
      @[simp]
      theorem Complex.UnitDisc.coe_zero :
      ↑0 = 0
      @[simp]
      @[simp]
      theorem Complex.UnitDisc.coe_smul_circle (z : { x // x ∈ circle }) (w : Complex.UnitDisc) :
      ↑(z β€’ w) = ↑z * ↑w
      @[simp]
      theorem Complex.UnitDisc.coe_smul_closedBall (z : ↑(Metric.closedBall 0 1)) (w : Complex.UnitDisc) :
      ↑(z β€’ w) = ↑z * ↑w

      Real part of a point of the unit disc.

      Instances For

        Imaginary part of a point of the unit disc.

        Instances For

          Conjugate point of the unit disc.

          Instances For