Linear maps over modules (#1395)

There's certainly more properties we can add here, but I ended up
building this as I was thinking about more general vector spaces.

(Because of the complexities around fields in constructive contexts --
e.g. that the reals aren't quite a field under the normal definition;
you have to substitute apartness from zero -- defining things in terms
of modules seems ideal where possible.)

---------

Co-authored-by: malarbol <[email protected]>

Author: lowasser

src/group-theory/abelian-groups.lagda.md

@@ -566,6 +566,23 @@ module _
   neg-right-subtraction-Ab = inv-right-div-Group (group-Ab A)
 ```
 
+### If `x + y = 0`, then `y ＝ -x` and `x ＝ -y`
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  abstract
+    unique-right-neg-Ab :
+      (x y : type-Ab A) → is-zero-Ab A (add-Ab A x y) → y ＝ neg-Ab A x
+    unique-right-neg-Ab = unique-right-inv-Group (group-Ab A)
+
+    unique-left-neg-Ab :
+      (x y : type-Ab A) → is-zero-Ab A (add-Ab A x y) → x ＝ neg-Ab A y
+    unique-left-neg-Ab = unique-left-inv-Group (group-Ab A)
+```
+
 ### The sum of `-x + y` and `-y + z` is `-x + z`
 
 ```agda

src/group-theory/groups.lagda.md

@@ -495,23 +495,24 @@ module _
   is-unit-right-div-eq-Group refl = right-inverse-law-mul-Group G _
 ```
 
-### If `xy = 1`, `y ＝ x⁻¹`
+### If `xy = 1`, then `y ＝ x⁻¹`
 
 ```agda
-  unique-right-inv-Group :
-    (x y : type-Group G) →
-    is-unit-Group G (mul-Group G x y) →
-    y ＝ inv-Group G x
-  unique-right-inv-Group x y xy=1 =
-    equational-reasoning
-      y
-      ＝ left-div-Group x (unit-Group G)
-        by transpose-eq-mul-Group' xy=1
-      ＝ inv-Group G x
-        by right-unit-law-mul-Group G (inv-Group G x)
+  abstract
+    unique-right-inv-Group :
+      (x y : type-Group G) →
+      is-unit-Group G (mul-Group G x y) →
+      y ＝ inv-Group G x
+    unique-right-inv-Group x y xy=1 =
+      equational-reasoning
+        y
+        ＝ left-div-Group x (unit-Group G)
+          by transpose-eq-mul-Group' xy=1
+        ＝ inv-Group G x
+          by right-unit-law-mul-Group G (inv-Group G x)
 ```
 
-### If `xy = 1`, `x ＝ y⁻¹`
+### If `xy = 1`, then `x ＝ y⁻¹`
 
 ```agda
   unique-left-inv-Group :

src/linear-algebra.lagda.md

@@ -14,9 +14,12 @@ open import linear-algebra.finite-sequences-in-euclidean-domains public
 open import linear-algebra.finite-sequences-in-rings public
 open import linear-algebra.finite-sequences-in-semirings public
 open import linear-algebra.functoriality-matrices public
+open import linear-algebra.left-modules-rings public
+open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.matrices public
 open import linear-algebra.matrices-on-rings public
 open import linear-algebra.multiplication-matrices public
+open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public
 open import linear-algebra.scalar-multiplication-tuples public
 open import linear-algebra.scalar-multiplication-tuples-on-rings public