1.19-3

delete some import
jjdishere · Jan 19, 2024 · 415d932 · 415d932
1 parent cf03c79
commit 415d932
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
@@ -1,9 +1,6 @@
-import EuclideanGeometry.Foundation.Axiom.Position.Orientation
-import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
 import EuclideanGeometry.Foundation.Axiom.Triangle.Trigonometric
 import EuclideanGeometry.Foundation.Axiom.Linear.Line_trash
 import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash
-import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular
 import EuclideanGeometry.Foundation.Axiom.Basic.Plane_trash
 import EuclideanGeometry.Foundation.Axiom.Position.Orientation_trash
 

diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean
@@ -1,5 +1,4 @@
 import EuclideanGeometry.Foundation.Axiom.Circle.Basic
-import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular_trash
 
 noncomputable section
 namespace EuclidGeom