search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

Update Basic/Angle.lean #266

Closed mbkybky closed 6 months ago

mbkybky commented 6 months ago

@jjdishere Main Changes:

  1. Add a new file to translate the theorems about trigonometric functions from the version of Real.sin, Real.cos or Real.tan to EuclidGeom.AngValue.sin, EuclidGeom.AngValue.cos or EuclidGeom.AngValue.tan
  2. Fill all sorrys in Basic/Angle.lean
  3. Clean the trash of Basic/Angle