jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

Axiom/Circle #265

Closed Noaillesss closed 6 months ago

Noaillesss commented 6 months ago

Basic: add some lemmas CirclePower: fill sorrys IncribedAngle: fill sorrys LCPosition: fix up, and finish the uniqueness of inx pts CCPosition: fix up

Perpendicular_trash: add theorems to say the perp_foot is unique Ray_trash: add two lemmas which are used in Angle_trash Angle_trash: add two theorems to describe special AngValue

Index: add a file path