### Abstract

A formalization of geometry of complex numbers is presented. Fundamental objects that are investigated are the complex plane extended by a single infinite point, its objects (points, lines and circles), and groups of transformations that act on them (e.g., inversions and Möbius transformations). Most objects are defined algebraically, but correspondence with classical geometric definitions is shown.

### License

BSD License

### Topics

- Mathematics/Geometry

### Session Complex_Geometry

- More_Transcendental
- Canonical_Angle
- More_Complex
- Angles
- More_Set
- Linear_Systems
- Quadratic
- Matrices
- Unitary_Matrices
- Unitary11_Matrices
- Hermitean_Matrices
- Elementary_Complex_Geometry
- Homogeneous_Coordinates
- Moebius
- Circlines
- Oriented_Circlines
- Circlines_Angle
- Unit_Circle_Preserving_Moebius
- Riemann_Sphere
- Chordal_Metric

### Used by

- Solving Cubic and Quartic Equations
- Poincaré Disc Model

## Cite

×

Complex_Geometry-AFP

    @article{Complex_Geometry-AFP,
      author  = {Filip Marić and Danijela Simić},
      title   = {Complex Geometry},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Complex_Geometry.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jan 17, 2020 : Isabelle2019