Toggle navigation
CertifiedETC
Lists of points
(current)
Transformation Tables
Complement
Anti-Complement
Isotomic Conjugate
Cyclocevian Conjugate
Isogonal Conjugate
Daleth Conjugate
Hirst inverse
Iso-Conjugate
Waw Conjugate
Line Conjugate
Ceva Conjugate
Cross Conjugate
Cross Point
Cross Sum
Coq files
About
Links
Credits
A Certified Version of Clark Kimberling's Encyclopedia of Triangle Centers
Formalization in Coq
Definition of the type of points
Definitions of the >6000 points
Conway's notations
Some invariance property of Conway's notations
Definition of some standard triangles, Cevian and anti-Cevian
Ceva conjugate
Complement and anti-complement
Cross conjugate
Cross difference
Cross point
Cross sum
Cyclocevian conjugate
Daleth conjugate
Hirst inverse
Iso conjugate
Isogonal conjugate
Isotomic conjugate
Waw conjugate
Zayin conjugate
Line conjugate
Lucas cubic
Midpoint
Pedal triangle
Circumcircle
Reflection
Definition of triangle centers
The triangle midpoint theorem
Varignon's theorem
Proof Tactics
Index