Merge remote-tracking branch 'origin/linear-maps' into linear-maps

Author: lowasser

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

@@ -566,7 +566,7 @@ module _
   neg-right-subtraction-Ab = inv-right-div-Group (group-Ab A)
 ```
 
-### If `x + y = 0`, `y ＝ -x` and `x ＝ -y`
+### If `x + y = 0`, then `y ＝ -x` and `x ＝ -y`
 
 ```agda
 module _

src/group-theory/groups.lagda.md

@@ -495,7 +495,7 @@ 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
   abstract
@@ -512,7 +512,7 @@ module _
           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/module-theory/linear-maps-left-modules-rings.lagda.md

@@ -1,4 +1,4 @@
-# Linear maps between modules over rings
+# Linear maps between left modules over rings
 
 ```agda
 module module-theory.linear-maps-left-modules-rings where
@@ -28,7 +28,7 @@ open import ring-theory.rings
 ## Idea
 
 A
-{{#concept "linear map" Agda=is-linear-map-left-module-Ring Disambiguation="over left modules" WD="linear map" WDID=Q207643 }}
+{{#concept "linear map" Agda=is-linear-map-left-module-Ring Disambiguation="over left modules over a ring" WD="linear map" WDID=Q207643 }}
 between [left modules](module-theory.left-modules-rings.md) is a map `f` with
 the following properties: