search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
27 stars 56 forks source link

Some refinement of Ray.lean, Line.lean, Triangle.lean, Similarity.lean and so on #271

Closed mbkybky closed 9 months ago

mbkybky commented 9 months ago

@jjdishere Main Changes:

  1. Some refinement of Ray.lean, Line.lean, Triangle.lean, Similarity.lean and so on. For example, change some def to abbrev.
  2. Try to discuss compatibility among group, addtorsor and order.