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
Topics
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