fixing merge

abelian_proof.py

@@ -24,4 +24,4 @@
 p.substituteRHS(11,12)
 p.identleft(13)
 p.forAllIntroduction(14,["a","b"],[1,2])
-p.qed(15)
+p.qed(15)

group.py

@@ -8,6 +8,7 @@ class group:
     elements = {}
     groupProperties = {} 
     elementProperties = {}
+    subGroups = []
     binaryOperator = ""
     groupName = ""
 
@@ -30,6 +31,12 @@ def __mul__(self,other): # group cartesian product. Worry about this later
         return group(newName, [self.binaryOperator,other.binaryOperator], newProperties)
 
     # group functions
+    def newInverse(self, elementName):
+        if elementName in self.elements:
+            inverseName =  '(' + elementName + ')^(-1)'
+            self.elements.update({inverseName:inverse(elementName,self)})
+        else:
+            print("Sorry, you cannot add the inverse of an element that does not exist!")
 
     # declare new element in group with elementName
     def newElement(self,elementName):
@@ -50,6 +57,10 @@ def mulElements(self, elem1, elem2): # should this return an equation?
                 self.elements.update({repr(result):result}) # is this the right?
             except:
                 print("Sorry, one or both of these elements are not in the group!")
+
+    def subGroup(self, property):
+        self.subGroups.append(property)
+        return f'{property} is a subgroup of {self}'
 
     def addGroupProperty(self, property, propertyName):
         self.groupProperties[propertyName] = property
@@ -67,4 +78,4 @@ def contains(self, elementName):
         return elementName in self.elements
 
     def toLaTeX(self):
-        return self.groupName
+        return self.groupName

logicObjects.py

@@ -244,6 +244,8 @@ def replace(self, replacements):
     def toLaTeX(self):
         return r"\exists " + ",".join(self.existelems) + r" \in " + str(self.group)  + r"\ " + self.toLaTeX(self.eq)
 
+
+
 ## Unique class - idk if we need this
 
 class uniqueElementProperty:

sub_group_proof.py

@@ -0,0 +1,20 @@
+from proof import *
+from element import *
+from group import *
+from integer import *
+from logicObjects import *
+
+G = group('G','*')
+subGroupG = G.subGroup(Eq('x',G.elements['e'],G))
+p = Proof('Simple Subgroup Proof', None, goal=subGroupG)
+p.introGroup(G)
+p.introSet('S',G,Eq('x',G.elements['e'],G)) # change to mult objects?
+p.getArbElem('S','a')
+p.getArbElem('S','b')
+p.multBothSides(2,3)
+p.identright(4)
+p.setClosure('S',[2,3],5)
+p.setContainsIdentity('S',2)
+p.setInverse('S',5)
+p.concludeSubgroup('S')
+p.qed(9)

sub_group_proof_2.py

@@ -0,0 +1,22 @@
+from proof import *
+from element import *
+from group import *
+from integer import *
+from logicObjects import *
+
+G = group('G','*')
+subGroupG = G.subGroup(In('x',G))
+p = Proof('Simple Subgroup Proof', None, goal=subGroupG)
+p.introGroup(G)
+p.introSet('S',G,In('x',G))
+p.getSpecificElem('S','e')
+p.setContainsIdentity('S',2)
+p.getArbElem('S','a')
+p.getArbElem('S','b')
+p.closure(G,'a','b')
+p.setClosure('S',[4,5],6)
+p.introInverse(G,'a')
+p.addElemToSet('S','(a)^(-1)',G)
+p.setInverse('S',8)
+p.concludeSubgroup('S')
+p.qed(11)