From a91eef113241805b1c68e4f43010d0640928538c Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 7 Feb 2024 15:08:03 -0600
Subject: [PATCH] new: Added some algebraic structures

---
 LeanTalkSP24.lean                |  2 ++
 LeanTalkSP24/alg_structures.lean | 41 ++++++++++++++++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 LeanTalkSP24/alg_structures.lean

diff --git a/LeanTalkSP24.lean b/LeanTalkSP24.lean
index c7928f8..b3acf04 100644
--- a/LeanTalkSP24.lean
+++ b/LeanTalkSP24.lean
@@ -4,3 +4,5 @@ import «LeanTalkSP24».basics
 import «LeanTalkSP24».basics2
 import «LeanTalkSP24».infinitely_many_primes
 import «LeanTalkSP24».polynomial_over_field_dim_one
+import «LeanTalkSP24».alg_structures
+
diff --git a/LeanTalkSP24/alg_structures.lean b/LeanTalkSP24/alg_structures.lean
new file mode 100644
index 0000000..0678ac3
--- /dev/null
+++ b/LeanTalkSP24/alg_structures.lean
@@ -0,0 +1,41 @@
+import Mathlib.Data.Real.Basic
+
+class Group₁ (α : Type _) where
+  mul : α → α → α
+  one : α
+  inv : α → α
+  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
+  mul_one : ∀ x : α, mul x one = x
+  one_mul : ∀ x : α, mul one x = x
+  mul_left_inv : ∀ x : α, mul (inv x) x = one
+
+@[ext]
+structure Point where
+  x : ℝ
+  y : ℝ
+  z : ℝ
+
+namespace Point
+
+def add (a b : Point) : Point :=
+  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
+
+def neg (a : Point) : Point := ⟨-a.x, -a.y, -a.z⟩
+
+def zero : Point := ⟨0,0,0⟩
+
+instance add_group_point: Group₁ Point where
+  mul := add
+  one := zero
+  inv := neg
+  mul_assoc := by simp [add, add_assoc]
+  mul_one := by simp [add, zero]
+  one_mul := by simp [add, zero]
+  mul_left_inv := by simp [add, neg, zero]
+
+end Point
+
+instance hasMulGroup₁ {α : Type _} [Group₁ α] : Add α := ⟨Group₁.mul⟩
+
+def v : Point := ⟨1,1,1⟩
+#check v+v