jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

Update AddToMathlib.lean, Vector.lean, Line.lean and Position/Angle.lean #274

Closed mbkybky closed 5 months ago

mbkybky commented 6 months ago

@jjdishere Main Changes: AddToMathlib.lean :

Vector.lean :

Line.lean :

  1. Realize a directed line as a linearly ordered AddTorsor
  2. Add induction principles to deduce results for directed lines or lines from those for rays
  3. Add some theorems about DirLine.ddist and fix some theorems

Position/Angle.lean :