search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

Update Basic/Angle.lean #259

Closed mbkybky closed 6 months ago

mbkybky commented 6 months ago

@jjdishere Main changes:

  1. Fill some sorrys in Basic/Angle.lean
  2. Add some planning theorems in Basic/Angle/FromMathlib.lean. Please check whether these theorems are necessary.