symgeoalg

commit 1bdb5df974c44722752b02bc33bfd6ff6f790552
parent 8e5293c0d74d288b11b6b5932eaf874e73c78fab
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Sat, 27 Jul 2024 15:16:06 -0700

Add Ring and Rat instance

Diffstat:
M
Main.lean
 | 
15
+++++++++++----

1 file changed, 11 insertions(+), 4 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -189,18 +189,25 @@ instance [MulGroup A] {n : Nat} : MulGroup (A ^ n) := MulGroup.instFun
 instance [MulCommGroup A] {n : Nat} : MulCommGroup (A ^ n) := MulCommGroup.instFun
 
 --------------------------------------------------------------------------------
--- Fields
+-- Rings, implicitly commutative and unital
 
--- Convention: (∀a. div a 0 = 0) and (inv 0 = 0).
-class Field (F : Type) extends AddGroup F, MulGroup F
+class Ring (R : Type) extends AddGroup R, MulMonoid R
 
-instance : Field Rat where
+instance : Ring Rat where
   zero := 0
   add := Rat.add
   sub := Rat.sub
   one := 1
   mul := Rat.mul
+
+--------------------------------------------------------------------------------
+-- Fields, where ∀a. div a = 0 and inv 0 = a
+
+class Field (F : Type) extends Ring F, MulGroup F
+
+instance : Field Rat where
   div := Rat.div
+  inv := Rat.inv
 
 --------------------------------------------------------------------------------
 -- Vector spaces