Merge pull request #14 from edegeltje/simple_docstrings

add some docstrings

equational_theories/Basic.lean

@@ -28,22 +28,30 @@ def Equation4 (G: Type*) [Magma G] := ∀ x y : G, x = x ∘ y
 /-- The right absorption law -/
 def Equation5 (G: Type*) [Magma G] := ∀ x y : G, x = y ∘ x
 
+@[inherit_doc Equation2]
 def Equation6 (G: Type*) [Magma G] := ∀ x y : G, x = y ∘ y
 
+@[inherit_doc Equation2]
 def Equation7 (G: Type*) [Magma G] := ∀ x y z : G, x = y ∘ z
 
 def Equation8 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ x)
 
+/-- value of multiplication is independent of right argument -/
 def Equation38 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = x ∘ y
 
+/-- value of multiplication is independent of left argument; dual of 38 -/
 def Equation39 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = y ∘ x
 
+/-- all squares are the same -/
 def Equation40 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = y ∘ y
 
+/-- all products are the same -/
 def Equation41 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ x = y ∘ z
 
+@[inherit_doc Equation38]
 def Equation42 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ y = x ∘ z
 
+/-- The commutative law -/
 def Equation43 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = y ∘ x
 
 /-- The constant law -/
@@ -61,6 +69,7 @@ def Equation4513 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ (y ∘ z) = (x 
 
 def Equation4552 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
 
+/-- all products of three values are the same, regardless bracketing -/
 def Equation4582 (G: Type*) [Magma G] := ∀ x y z w u v: G, x ∘ (y ∘ z) = (w ∘ u) ∘ v