Session Complex_Geometry
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Periodic_Fun
More_Transcendental
Canonical_Angle
More_Complex
Angles
More_Set
Linear_Systems
HOL-Library.Quadratic_Discriminant
Quadratic
Matrices
Unitary_Matrices
Unitary11_Matrices
Hermitean_Matrices
Elementary_Complex_Geometry
Homogeneous_Coordinates
Moebius
Circlines
Oriented_Circlines
Circlines_Angle
Unit_Circle_Preserving_Moebius
HOL-Library.Product_Plus
HOL-Analysis.Product_Vector
Riemann_Sphere
HOL-Analysis.Inner_Product
HOL-Analysis.L2_Norm
HOL-Analysis.Euclidean_Space
Chordal_Metric