Vector Major Update

changed the foundation from being building upon R x R to C
jjdishere · Sep 18, 2023 · f912a80 · f912a80
1 parent a1ba889
commit f912a80
Show file tree

Hide file tree

Showing 6 changed files with 1,162 additions and 355 deletions.
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
@@ -29,7 +29,7 @@ noncomputable section
 namespace EuclidGeom
 
 /- Define Euclidean plane as normed vector space over ℝ of dimension 2 -/
-class EuclideanPlane (P : Type _) extends MetricSpace P, @NormedAddTorsor (Vec) P Vec.SeminormedAddCommGroup _
+class EuclideanPlane (P : Type _) extends MetricSpace P, @NormedAddTorsor Vec P _ _
 
 variable  {P : Type _} [EuclideanPlane P] 
 
@@ -38,10 +38,10 @@ def Vec.mk_pt_pt (A B : P) : (Vec) := (B -ᵥ A)
 scoped notation "VEC" => Vec.mk_pt_pt
 
 instance : EuclideanPlane (Vec) where
-  toMetricSpace := Vec.MetricSpace
-  toNormedAddTorsor := @SeminormedAddCommGroup.toNormedAddTorsor _ Vec.SeminormedAddCommGroup
+  toMetricSpace := _
+  toNormedAddTorsor := @SeminormedAddCommGroup.toNormedAddTorsor _ _
 
-instance : @NormedAddTorsor (Vec) P Vec.SeminormedAddCommGroup _ := EuclideanPlane.toNormedAddTorsor
+instance : @NormedAddTorsor (Vec) P _ _ := EuclideanPlane.toNormedAddTorsor
 
 instance : AddTorsor (Vec) P := by infer_instance