diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 4ebddac443d..64ea0afcd92 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -452,6 +452,7 @@ open import foundation.similarity-preserving-maps-large-similarity-relations pub
 open import foundation.similarity-subtypes public
 open import foundation.singleton-induction public
 open import foundation.singleton-subtypes public
+open import foundation.singleton-subtypes-discrete-types public
 open import foundation.slice public
 open import foundation.small-maps public
 open import foundation.small-types public
diff --git a/src/foundation/singleton-subtypes-discrete-types.lagda.md b/src/foundation/singleton-subtypes-discrete-types.lagda.md
new file mode 100644
index 00000000000..02ef8ef27b5
--- /dev/null
+++ b/src/foundation/singleton-subtypes-discrete-types.lagda.md
@@ -0,0 +1,89 @@
+# Singleton subtypes of discrete types
+
+```agda
+module foundation.singleton-subtypes-discrete-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.decidable-subtypes
+open import foundation.dependent-pair-types
+open import foundation.discrete-types
+open import foundation.functoriality-coproduct-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.singleton-subtypes
+open import foundation.universe-levels
+
+open import foundation-core.subtypes
+open import foundation-core.transport-along-identifications
+```
+
+</details>
+
+## Idea
+
+[Singleton subtypes](foundation.singleton-subtypes.md) on
+[discrete types](foundation.discrete-types.md) are
+[decidable subtypes](foundation.decidable-subtypes.md).
+
+## Properties
+
+### Any singleton subtype of a discrete type is decidable
+
+```agda
+module _
+  {l1 l2 : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l1)
+  (S : subtype l2 X)
+  (((x , x∈S) , is-center-x) : is-singleton-subtype S)
+  where
+
+  is-decidable-is-singleton-subtype-Discrete-Type : is-decidable-subtype S
+  is-decidable-is-singleton-subtype-Discrete-Type y =
+    map-coproduct
+      ( λ x=y → tr (is-in-subtype S) x=y x∈S)
+      ( λ x≠y y∈S → x≠y (ap (inclusion-subtype S) (is-center-x (y , y∈S))))
+      ( decide-eq-X x y)
+```
+
+### The standard decidable singleton subtype associated with an element of a discrete type
+
+```agda
+module _
+  {l : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l)
+  where
+
+  decidable-standard-singleton-subtype-Discrete-Type :
+    X → decidable-subtype l X
+  decidable-standard-singleton-subtype-Discrete-Type y x =
+    ( x ＝ y ,
+      is-set-type-Discrete-Type XD x y ,
+      decide-eq-X x y)
+```
+
+### The standard decidable singleton subtype is contractible
+
+```agda
+module _
+  {l : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l)
+  (x : X)
+  where
+
+  is-contr-type-decidable-standard-singleton-subtype-Discrete-Type :
+    is-contr
+      ( type-decidable-subtype
+        ( decidable-standard-singleton-subtype-Discrete-Type XD x))
+  is-contr-type-decidable-standard-singleton-subtype-Discrete-Type =
+    ( (x , refl) ,
+      λ (y , x=y) →
+        eq-type-subtype
+          ( subtype-decidable-subtype
+            ( decidable-standard-singleton-subtype-Discrete-Type XD x))
+          ( inv x=y))
+```
diff --git a/src/group-theory/invertible-elements-monoids.lagda.md b/src/group-theory/invertible-elements-monoids.lagda.md
index d4afd9a796b..c9d8e58fc69 100644
--- a/src/group-theory/invertible-elements-monoids.lagda.md
+++ b/src/group-theory/invertible-elements-monoids.lagda.md
@@ -168,6 +168,9 @@ module _
     is-invertible-element-Monoid M x
   pr2 (is-invertible-element-prop-Monoid x) =
     is-prop-is-invertible-element-Monoid x
+
+  invertible-element-Monoid : UU l
+  invertible-element-Monoid = type-subtype is-invertible-element-prop-Monoid
 ```
 
 ### Inverses are left/right inverses
@@ -292,6 +295,11 @@ module _
     left-unit-law-mul-Monoid M (unit-Monoid M)
   pr2 (pr2 is-invertible-element-unit-Monoid) =
     left-unit-law-mul-Monoid M (unit-Monoid M)
+
+  invertible-element-unit-Monoid :
+    invertible-element-Monoid M
+  invertible-element-unit-Monoid =
+    ( unit-Monoid M , is-invertible-element-unit-Monoid)
 ```
 
 ### Invertible elements are closed under multiplication
@@ -350,6 +358,14 @@ module _
       ( is-left-invertible-element-mul-Monoid x y
         ( is-left-invertible-is-invertible-element-Monoid M x H)
         ( is-left-invertible-is-invertible-element-Monoid M y K))
+
+  mul-invertible-element-Monoid :
+    invertible-element-Monoid M →
+    invertible-element-Monoid M →
+    invertible-element-Monoid M
+  mul-invertible-element-Monoid (x , is-inv-x) (y , is-inv-y) =
+    ( mul-Monoid M x y ,
+      is-invertible-element-mul-Monoid x y is-inv-x is-inv-y)
 ```
 
 ### The inverse of an invertible element is invertible
@@ -367,6 +383,12 @@ module _
     is-left-inverse-inv-is-invertible-element-Monoid M H
   pr2 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
     is-right-inverse-inv-is-invertible-element-Monoid M H
+
+  invertible-element-inv-invertible-element-Monoid :
+    invertible-element-Monoid M → invertible-element-Monoid M
+  invertible-element-inv-invertible-element-Monoid (x , is-invertible-x) =
+    ( inv-is-invertible-element-Monoid M is-invertible-x ,
+      is-invertible-element-inv-is-invertible-element-Monoid is-invertible-x)
 ```
 
 ### An element is invertible if and only if multiplying by it is an equivalence
@@ -400,25 +422,27 @@ module _
   inv-is-invertible-element-is-equiv-mul-Monoid H =
     map-inv-is-equiv H (unit-Monoid M)
 
-  is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
-    (H : is-equiv (mul-Monoid M x)) →
-    mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid H) ＝
-    unit-Monoid M
-  is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
-    is-section-map-inv-is-equiv H (unit-Monoid M)
-
-  is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
-    (H : is-equiv (mul-Monoid M x)) →
-    mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid H) x ＝
-    unit-Monoid M
-  is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
-    is-injective-is-equiv H
-      ( ( inv (associative-mul-Monoid M _ _ _)) ∙
-        ( ap
-          ( mul-Monoid' M x)
-          ( is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H)) ∙
-        ( left-unit-law-mul-Monoid M x) ∙
-        ( inv (right-unit-law-mul-Monoid M x)))
+  abstract
+    is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
+      (H : is-equiv (mul-Monoid M x)) →
+      mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid H) ＝
+      unit-Monoid M
+    is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
+      is-section-map-inv-is-equiv H (unit-Monoid M)
+
+    is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
+      (H : is-equiv (mul-Monoid M x)) →
+      mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid H) x ＝
+      unit-Monoid M
+    is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
+      is-injective-is-equiv H
+        ( ( inv (associative-mul-Monoid M _ _ _)) ∙
+          ( ap
+            ( mul-Monoid' M x)
+            ( is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid
+              ( H))) ∙
+          ( left-unit-law-mul-Monoid M x) ∙
+          ( inv (right-unit-law-mul-Monoid M x)))
 
   is-invertible-element-is-equiv-mul-Monoid :
     is-equiv (mul-Monoid M x) → is-invertible-element-Monoid M x
@@ -434,25 +458,26 @@ module _
   left-div-is-invertible-element-Monoid H =
     mul-Monoid M (inv-is-invertible-element-Monoid M H)
 
-  is-section-left-div-is-invertible-element-Monoid :
-    (H : is-invertible-element-Monoid M x) →
-    mul-Monoid M x ∘ left-div-is-invertible-element-Monoid H ~ id
-  is-section-left-div-is-invertible-element-Monoid H y =
-    ( inv (associative-mul-Monoid M _ _ _)) ∙
-    ( ap
-      ( mul-Monoid' M y)
-      ( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙
-    ( left-unit-law-mul-Monoid M y)
-
-  is-retraction-left-div-is-invertible-element-Monoid :
-    (H : is-invertible-element-Monoid M x) →
-    left-div-is-invertible-element-Monoid H ∘ mul-Monoid M x ~ id
-  is-retraction-left-div-is-invertible-element-Monoid H y =
-    ( inv (associative-mul-Monoid M _ _ _)) ∙
-    ( ap
-      ( mul-Monoid' M y)
-      ( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙
-    ( left-unit-law-mul-Monoid M y)
+  abstract
+    is-section-left-div-is-invertible-element-Monoid :
+      (H : is-invertible-element-Monoid M x) →
+      mul-Monoid M x ∘ left-div-is-invertible-element-Monoid H ~ id
+    is-section-left-div-is-invertible-element-Monoid H y =
+      ( inv (associative-mul-Monoid M _ _ _)) ∙
+      ( ap
+        ( mul-Monoid' M y)
+        ( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙
+      ( left-unit-law-mul-Monoid M y)
+
+    is-retraction-left-div-is-invertible-element-Monoid :
+      (H : is-invertible-element-Monoid M x) →
+      left-div-is-invertible-element-Monoid H ∘ mul-Monoid M x ~ id
+    is-retraction-left-div-is-invertible-element-Monoid H y =
+      ( inv (associative-mul-Monoid M _ _ _)) ∙
+      ( ap
+        ( mul-Monoid' M y)
+        ( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙
+      ( left-unit-law-mul-Monoid M y)
 
   is-equiv-mul-is-invertible-element-Monoid :
     is-invertible-element-Monoid M x → is-equiv (mul-Monoid M x)
diff --git a/src/group-theory/products-of-finite-families-of-elements-commutative-monoids.lagda.md b/src/group-theory/products-of-finite-families-of-elements-commutative-monoids.lagda.md
index c7aa502734c..8bb6f872e2f 100644
--- a/src/group-theory/products-of-finite-families-of-elements-commutative-monoids.lagda.md
+++ b/src/group-theory/products-of-finite-families-of-elements-commutative-monoids.lagda.md
@@ -37,6 +37,7 @@ open import foundation.universal-property-propositional-truncation-into-sets
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.homomorphisms-commutative-monoids
 open import group-theory.products-of-finite-families-of-elements-commutative-semigroups
 open import group-theory.products-of-finite-sequences-of-elements-commutative-monoids
 
@@ -781,3 +782,52 @@ module _
           ( product-unit-finite-Commutative-Monoid M _))) ∙
       ( right-unit-law-mul-Commutative-Monoid M _)
 ```
+
+### Commutative monoid homomorphisms distribute over finite sums
+
+```agda
+abstract
+  distributive-hom-product-finite-Commutative-Monoid :
+    {l1 l2 l3 : Level} (M : Commutative-Monoid l1) (N : Commutative-Monoid l2)
+    (φ : hom-Commutative-Monoid M N) (A : Finite-Type l3)
+    (u : type-Finite-Type A → type-Commutative-Monoid M) →
+    map-hom-Commutative-Monoid M N φ
+      ( product-finite-Commutative-Monoid M A u) ＝
+    product-finite-Commutative-Monoid N A (map-hom-Commutative-Monoid M N φ ∘ u)
+  distributive-hom-product-finite-Commutative-Monoid M N φ FA@(A , is-fin-A) u =
+    rec-trunc-Prop
+      ( Id-Prop
+        ( set-Commutative-Monoid N)
+        ( map-hom-Commutative-Monoid M N φ
+          ( product-finite-Commutative-Monoid M FA u))
+        ( product-finite-Commutative-Monoid N FA
+          ( map-hom-Commutative-Monoid M N φ ∘ u)))
+      ( λ cA →
+        equational-reasoning
+          map-hom-Commutative-Monoid M N φ
+            ( product-finite-Commutative-Monoid M FA u)
+          ＝
+            map-hom-Commutative-Monoid M N φ
+              ( product-count-Commutative-Monoid M A cA u)
+            by
+              ap
+                ( map-hom-Commutative-Monoid M N φ)
+                ( eq-product-finite-product-count-Commutative-Monoid M FA cA u)
+          ＝
+            product-count-Commutative-Monoid N A cA
+              ( map-hom-Commutative-Monoid M N φ ∘ u)
+            by
+              distributive-hom-product-fin-sequence-type-Commutative-Monoid
+                ( M)
+                ( N)
+                ( φ)
+                ( _)
+                ( _)
+          ＝
+            product-finite-Commutative-Monoid N FA
+              ( map-hom-Commutative-Monoid M N φ ∘ u)
+            by
+              inv
+                ( eq-product-finite-product-count-Commutative-Monoid N FA cA _))
+      ( is-fin-A)
+```
diff --git a/src/group-theory/products-of-finite-sequences-of-elements-commutative-monoids.lagda.md b/src/group-theory/products-of-finite-sequences-of-elements-commutative-monoids.lagda.md
index 788738eee70..646b956407f 100644
--- a/src/group-theory/products-of-finite-sequences-of-elements-commutative-monoids.lagda.md
+++ b/src/group-theory/products-of-finite-sequences-of-elements-commutative-monoids.lagda.md
@@ -315,6 +315,24 @@ hom-product-fin-sequence-type-Commutative-Monoid M n =
     product-unit-fin-sequence-type-Commutative-Monoid M n)
 ```
 
+### Commutative monoid homomorphisms distribute over the product operation
+
+```agda
+abstract
+  distributive-hom-product-fin-sequence-type-Commutative-Monoid :
+    {l1 l2 : Level} (M : Commutative-Monoid l1) (N : Commutative-Monoid l2)
+    (φ : hom-Commutative-Monoid M N)
+    (n : ℕ) (u : fin-sequence-type-Commutative-Monoid M n) →
+    map-hom-Commutative-Monoid M N φ
+      ( product-fin-sequence-type-Commutative-Monoid M n u) ＝
+    product-fin-sequence-type-Commutative-Monoid N n
+      ( map-hom-Commutative-Monoid M N φ ∘ u)
+  distributive-hom-product-fin-sequence-type-Commutative-Monoid M N =
+    distributive-hom-product-fin-sequence-type-Monoid
+      ( monoid-Commutative-Monoid M)
+      ( monoid-Commutative-Monoid N)
+```
+
 ## See also
 
 - [Products of finite families of elements in commutative monoids](group-theory.products-of-finite-families-of-elements-commutative-monoids.md)
diff --git a/src/group-theory/products-of-finite-sequences-of-elements-groups.lagda.md b/src/group-theory/products-of-finite-sequences-of-elements-groups.lagda.md
index aee61a6b936..2e58ced71ce 100644
--- a/src/group-theory/products-of-finite-sequences-of-elements-groups.lagda.md
+++ b/src/group-theory/products-of-finite-sequences-of-elements-groups.lagda.md
@@ -20,6 +20,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import group-theory.groups
+open import group-theory.homomorphisms-groups
 open import group-theory.powers-of-elements-groups
 open import group-theory.products-of-finite-sequences-of-elements-monoids
 
@@ -187,3 +188,19 @@ abstract
   product-constant-fin-sequence-type-Group G =
     product-constant-fin-sequence-type-Monoid (monoid-Group G)
 ```
+
+### Group homomorphisms distribute over products
+
+```agda
+abstract
+  distributive-hom-product-fin-sequence-type-Group :
+    {l1 l2 : Level} (G : Group l1) (H : Group l2) (φ : hom-Group G H) →
+    (n : ℕ) (u : fin-sequence-type-Group G n) →
+    map-hom-Group G H φ (product-fin-sequence-type-Group G n u) ＝
+    product-fin-sequence-type-Group H n (map-hom-Group G H φ ∘ u)
+  distributive-hom-product-fin-sequence-type-Group G H φ =
+    distributive-hom-product-fin-sequence-type-Monoid
+      ( monoid-Group G)
+      ( monoid-Group H)
+      ( hom-monoid-hom-Group G H φ)
+```
diff --git a/src/group-theory/products-of-finite-sequences-of-elements-monoids.lagda.md b/src/group-theory/products-of-finite-sequences-of-elements-monoids.lagda.md
index 7a56f01dcdb..6d5caabc975 100644
--- a/src/group-theory/products-of-finite-sequences-of-elements-monoids.lagda.md
+++ b/src/group-theory/products-of-finite-sequences-of-elements-monoids.lagda.md
@@ -19,6 +19,7 @@ open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
+open import group-theory.homomorphisms-monoids
 open import group-theory.monoids
 open import group-theory.powers-of-elements-monoids
 
@@ -222,3 +223,21 @@ abstract
       ( product-constant-fin-sequence-type-Monoid M n x)
       ( refl)
 ```
+
+### Monoid homomorphisms distribute over products
+
+```agda
+abstract
+  distributive-hom-product-fin-sequence-type-Monoid :
+    {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (φ : hom-Monoid M N) →
+    (n : ℕ) (u : fin-sequence-type-Monoid M n) →
+    map-hom-Monoid M N φ (product-fin-sequence-type-Monoid M n u) ＝
+    product-fin-sequence-type-Monoid N n (map-hom-Monoid M N φ ∘ u)
+  distributive-hom-product-fin-sequence-type-Monoid M N φ 0 u =
+    preserves-unit-hom-Monoid M N φ
+  distributive-hom-product-fin-sequence-type-Monoid M N φ (succ-ℕ n) u =
+    ( preserves-mul-hom-Monoid M N φ) ∙
+    ( ap-mul-Monoid N
+      ( distributive-hom-product-fin-sequence-type-Monoid M N φ n (u ∘ inl))
+      ( refl))
+```
diff --git a/src/group-theory/sums-of-finite-families-of-elements-abelian-groups.lagda.md b/src/group-theory/sums-of-finite-families-of-elements-abelian-groups.lagda.md
index 10c35409ef8..be0da0d51c8 100644
--- a/src/group-theory/sums-of-finite-families-of-elements-abelian-groups.lagda.md
+++ b/src/group-theory/sums-of-finite-families-of-elements-abelian-groups.lagda.md
@@ -8,12 +8,14 @@ module group-theory.sums-of-finite-families-of-elements-abelian-groups where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.sets
 open import foundation.type-arithmetic-cartesian-product-types
@@ -21,11 +23,14 @@ open import foundation.unit-type
 open import foundation.universe-levels
 
 open import group-theory.abelian-groups
+open import group-theory.homomorphisms-abelian-groups
 open import group-theory.products-of-finite-families-of-elements-commutative-monoids
 open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
 
+open import univalent-combinatorics.complements-decidable-subtypes
 open import univalent-combinatorics.coproduct-types
 open import univalent-combinatorics.counting
+open import univalent-combinatorics.decidable-subtypes
 open import univalent-combinatorics.dependent-pair-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.standard-finite-types
@@ -79,7 +84,7 @@ module _
 ```agda
 module _
   {l : Level} (G : Ab l)
-  where
+  where abstract
 
   htpy-sum-finite-Ab :
     {l2 : Level} (A : Finite-Type l2) →
@@ -94,7 +99,7 @@ module _
 ```agda
 module _
   {l : Level} (G : Ab l)
-  where
+  where abstract
 
   sum-zero-finite-Ab :
     {l2 : Level} (A : Finite-Type l2) →
@@ -109,7 +114,7 @@ module _
 module _
   {l1 l2 l3 : Level} (G : Ab l1) (A : Finite-Type l2) (B : Finite-Type l3)
   (H : equiv-Finite-Type A B)
-  where
+  where abstract
 
   sum-equiv-finite-Ab :
     (f : type-Finite-Type A → type-Ab G) →
@@ -127,7 +132,7 @@ module _
 ```agda
 module _
   {l1 l2 l3 : Level} (G : Ab l1) (A : Finite-Type l2) (B : Finite-Type l3)
-  where
+  where abstract
 
   distributive-sum-coproduct-finite-Ab :
     (f :
@@ -150,7 +155,7 @@ module _
 module _
   {l1 l2 l3 : Level} (G : Ab l1)
   (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3)
-  where
+  where abstract
 
   sum-Σ-finite-Ab :
     (f : (a : type-Finite-Type A) → type-Finite-Type (B a) → type-Ab G) →
@@ -166,7 +171,7 @@ module _
 module _
   {l1 l2 : Level} (G : Ab l1) (A : Finite-Type l2)
   (H : is-empty (type-Finite-Type A))
-  where
+  where abstract
 
   eq-zero-sum-finite-is-empty-Ab :
     (f : type-Finite-Type A → type-Ab G) →
@@ -197,7 +202,7 @@ eq-sum-finite-sum-count-Ab G =
 ```agda
 module _
   {l1 l2 : Level} (G : Ab l1) (A : Finite-Type l2)
-  where
+  where abstract
 
   interchange-sum-add-finite-Ab :
     (f g : type-Finite-Type A → type-Ab G) →
@@ -232,3 +237,78 @@ module _
             by htpy-sum-finite-Ab G A (λ a → right-inverse-law-add-Ab G _)
           ＝ zero-Ab G by sum-zero-finite-Ab G A)
 ```
+
+### Sums that vanish on a decidable subtype
+
+```agda
+module _
+  {l1 l2 l3 : Level} (G : Ab l1) (A : Finite-Type l2)
+  (P : subset-Finite-Type l3 A)
+  where
+
+  abstract
+    vanish-sum-decidable-subset-finite-Ab :
+      (f : type-Finite-Type A → type-Ab G) →
+      ( (a : type-Finite-Type A) → is-in-decidable-subtype P a →
+        is-zero-Ab G (f a)) →
+      sum-finite-Ab G A f ＝
+      sum-finite-Ab G
+        ( finite-type-complement-subset-Finite-Type A P)
+        ( f ∘ inclusion-complement-subset-Finite-Type A P)
+    vanish-sum-decidable-subset-finite-Ab =
+      vanish-product-decidable-subset-finite-Commutative-Monoid
+        ( commutative-monoid-Ab G)
+        ( A)
+        ( P)
+
+    vanish-sum-complement-decidable-subset-finite-Ab :
+      (f : type-Finite-Type A → type-Ab G) →
+      ( (a : type-Finite-Type A) → ¬ (is-in-decidable-subtype P a) →
+        is-zero-Ab G (f a)) →
+      sum-finite-Ab G A f ＝
+      sum-finite-Ab G
+        ( finite-type-subset-Finite-Type A P)
+        ( f ∘ inclusion-subset-Finite-Type A P)
+    vanish-sum-complement-decidable-subset-finite-Ab =
+      vanish-product-complement-decidable-subset-finite-Commutative-Monoid
+        ( commutative-monoid-Ab G)
+        ( A)
+        ( P)
+```
+
+### Sums over contractible types
+
+```agda
+module _
+  {l1 l2 : Level} (G : Ab l1) (I : Finite-Type l2)
+  (is-contr-I : is-contr (type-Finite-Type I))
+  (i : type-Finite-Type I)
+  where
+
+  abstract
+    sum-finite-is-contr-Ab :
+      (f : type-Finite-Type I → type-Ab G) →
+      sum-finite-Ab G I f ＝ f i
+    sum-finite-is-contr-Ab =
+      product-finite-is-contr-Commutative-Monoid
+        ( commutative-monoid-Ab G)
+        ( I)
+        ( is-contr-I)
+        ( i)
+```
+
+### Abelian group homomorphisms distribute over finite sums
+
+```agda
+abstract
+  distributive-hom-sum-finite-Ab :
+    {l1 l2 l3 : Level} (G : Ab l1) (H : Ab l2) (φ : hom-Ab G H)
+    (I : Finite-Type l3) (u : type-Finite-Type I → type-Ab G) →
+    map-hom-Ab G H φ (sum-finite-Ab G I u) ＝
+    sum-finite-Ab H I (map-hom-Ab G H φ ∘ u)
+  distributive-hom-sum-finite-Ab G H φ =
+    distributive-hom-product-finite-Commutative-Monoid
+      ( commutative-monoid-Ab G)
+      ( commutative-monoid-Ab H)
+      ( hom-commutative-monoid-hom-Ab G H φ)
+```
diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md
index e0436da8639..7059e3b434a 100644
--- a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md
+++ b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md
@@ -344,6 +344,21 @@ module _
       ( neg-right-subtraction-Ab G _ _)
 ```
 
+### Abelian group homomorphisms distribute over sums
+
+```agda
+abstract
+  distributive-hom-sum-fin-sequence-type-Ab :
+    {l1 l2 : Level} (G : Ab l1) (H : Ab l2) (φ : hom-Ab G H) →
+    (n : ℕ) (u : fin-sequence-type-Ab G n) →
+    map-hom-Ab G H φ (sum-fin-sequence-type-Ab G n u) ＝
+    sum-fin-sequence-type-Ab H n (map-hom-Ab G H φ ∘ u)
+  distributive-hom-sum-fin-sequence-type-Ab G H =
+    distributive-hom-product-fin-sequence-type-Group
+      ( group-Ab G)
+      ( group-Ab H)
+```
+
 ## See also
 
 - [Products of finite families of elements in commutative monoids](group-theory.products-of-finite-families-of-elements-commutative-monoids.md)
diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index dfe35b96461..bbfe7793428 100644
--- a/src/linear-algebra.lagda.md
+++ b/src/linear-algebra.lagda.md
@@ -7,6 +7,7 @@ module linear-algebra where
 
 open import linear-algebra.addition-linear-maps-left-modules-commutative-rings public
 open import linear-algebra.addition-linear-maps-left-modules-rings public
+open import linear-algebra.algebra-of-square-matrices-on-commutative-rings public
 open import linear-algebra.bilinear-forms-real-vector-spaces public
 open import linear-algebra.bilinear-maps-left-modules-commutative-rings public
 open import linear-algebra.bilinear-maps-left-modules-rings public
@@ -15,15 +16,19 @@ open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces p
 open import linear-algebra.complex-inner-product-spaces public
 open import linear-algebra.complex-vector-spaces public
 open import linear-algebra.conjugate-symmetric-sesquilinear-forms-complex-vector-spaces public
-open import linear-algebra.constant-matrices public
+open import linear-algebra.constant-grids public
 open import linear-algebra.constant-tuples public
 open import linear-algebra.dependent-products-left-modules-commutative-rings public
 open import linear-algebra.dependent-products-left-modules-rings public
 open import linear-algebra.dependent-products-real-vector-spaces public
 open import linear-algebra.dependent-products-vector-spaces public
+open import linear-algebra.diagonal-grids-on-rings public
 open import linear-algebra.diagonal-matrices-on-rings public
+open import linear-algebra.diagonals-of-square-matrices public
 open import linear-algebra.difference-linear-maps-left-modules-commutative-rings public
 open import linear-algebra.difference-linear-maps-left-modules-rings public
+open import linear-algebra.dot-product-finite-sequences-in-commutative-rings public
+open import linear-algebra.dot-product-finite-sequences-in-rings public
 open import linear-algebra.dot-product-standard-euclidean-vector-spaces public
 open import linear-algebra.duals-left-modules-commutative-rings public
 open import linear-algebra.finite-sequences-in-abelian-groups public
@@ -40,7 +45,14 @@ open import linear-algebra.finite-sequences-in-semirings public
 open import linear-algebra.function-left-modules-rings public
 open import linear-algebra.function-real-vector-spaces public
 open import linear-algebra.function-vector-spaces public
-open import linear-algebra.functoriality-matrices public
+open import linear-algebra.functoriality-grids public
+open import linear-algebra.general-linear-groups-finite-degree-rings public
+open import linear-algebra.grids public
+open import linear-algebra.grids-on-rings public
+open import linear-algebra.identity-matrices-on-commutative-rings public
+open import linear-algebra.identity-matrices-on-rings public
+open import linear-algebra.indicator-finite-sequences-in-commutative-rings public
+open import linear-algebra.indicator-finite-sequences-in-rings public
 open import linear-algebra.kernels-linear-maps-left-modules-commutative-rings public
 open import linear-algebra.kernels-linear-maps-left-modules-rings public
 open import linear-algebra.kernels-linear-maps-vector-spaces public
@@ -61,8 +73,14 @@ open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.linear-maps-vector-spaces public
 open import linear-algebra.linear-spans-left-modules-rings public
 open import linear-algebra.matrices public
+open import linear-algebra.matrices-on-commutative-rings public
 open import linear-algebra.matrices-on-rings public
-open import linear-algebra.multiplication-matrices public
+open import linear-algebra.multiplication-diagonal-matrices-rings public
+open import linear-algebra.multiplication-grids public
+open import linear-algebra.multiplication-matrices-on-commutative-rings public
+open import linear-algebra.multiplication-matrices-on-rings public
+open import linear-algebra.multiplication-square-matrices-on-commutative-rings public
+open import linear-algebra.multiplication-square-matrices-on-rings public
 open import linear-algebra.negation-linear-maps-left-modules-rings public
 open import linear-algebra.normed-complex-vector-spaces public
 open import linear-algebra.normed-real-vector-spaces public
@@ -77,21 +95,29 @@ open import linear-algebra.real-inner-product-spaces public
 open import linear-algebra.real-inner-product-spaces-are-normed public
 open import linear-algebra.real-vector-spaces public
 open import linear-algebra.right-modules-rings public
+open import linear-algebra.rings-of-square-matrices-on-rings public
+open import linear-algebra.scalar-multiplication-grids public
 open import linear-algebra.scalar-multiplication-linear-maps-left-modules-commutative-rings public
 open import linear-algebra.scalar-multiplication-linear-maps-vector-spaces 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
 open import linear-algebra.seminormed-complex-vector-spaces public
 open import linear-algebra.seminormed-real-vector-spaces public
 open import linear-algebra.sesquilinear-forms-complex-vector-spaces public
+open import linear-algebra.square-matrices public
+open import linear-algebra.square-matrices-on-commutative-rings public
+open import linear-algebra.square-matrices-on-rings public
 open import linear-algebra.standard-euclidean-inner-product-spaces public
 open import linear-algebra.standard-euclidean-vector-spaces public
 open import linear-algebra.subsets-left-modules-commutative-rings public
 open import linear-algebra.subsets-left-modules-rings public
 open import linear-algebra.subspaces-vector-spaces public
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-commutative-rings public
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-rings public
 open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public
 open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
+open import linear-algebra.symmetric-matrices public
+open import linear-algebra.transposition-grids public
 open import linear-algebra.transposition-matrices public
 open import linear-algebra.tuples-on-commutative-monoids public
 open import linear-algebra.tuples-on-commutative-rings public
diff --git a/src/linear-algebra/algebra-of-square-matrices-on-commutative-rings.lagda.md b/src/linear-algebra/algebra-of-square-matrices-on-commutative-rings.lagda.md
new file mode 100644
index 00000000000..1f8af20a315
--- /dev/null
+++ b/src/linear-algebra/algebra-of-square-matrices-on-commutative-rings.lagda.md
@@ -0,0 +1,78 @@
+# The algebra of square matrices on commutative rings
+
+```agda
+module linear-algebra.algebra-of-square-matrices-on-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.algebras-commutative-rings
+open import commutative-algebra.associative-algebras-commutative-rings
+open import commutative-algebra.commutative-rings
+open import commutative-algebra.unital-associative-algebras-commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import group-theory.monoids
+
+open import linear-algebra.identity-matrices-on-commutative-rings
+open import linear-algebra.multiplication-square-matrices-on-commutative-rings
+open import linear-algebra.square-matrices-on-commutative-rings
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+[Square matrices](linear-algebra.square-matrices-on-commutative-rings.md) on
+[commutative rings](commutative-algebra.commutative-rings.md) form a
+[unital associative algebra](commutative-algebra.unital-associative-algebras-commutative-rings.md)
+under
+[matrix multiplication](linear-algebra.multiplication-square-matrices-on-commutative-rings.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  algebra-square-matrix-Commutative-Ring : algebra-Commutative-Ring l R
+  algebra-square-matrix-Commutative-Ring =
+    ( left-module-square-matrix-Commutative-Ring R n ,
+      bilinear-map-mul-square-matrix-Commutative-Ring R n)
+
+  associative-algebra-square-matrix-Commutative-Ring :
+    associative-algebra-Commutative-Ring l R
+  associative-algebra-square-matrix-Commutative-Ring =
+    ( algebra-square-matrix-Commutative-Ring ,
+      associative-mul-square-matrix-Commutative-Ring R n)
+
+  unital-associative-algebra-square-matrix-Commutative-Ring :
+    unital-associative-algebra-Commutative-Ring l R
+  unital-associative-algebra-square-matrix-Commutative-Ring =
+    ( associative-algebra-square-matrix-Commutative-Ring ,
+      id-matrix-Commutative-Ring R n ,
+      left-unit-law-mul-square-matrix-Commutative-Ring R n ,
+      right-unit-law-mul-square-matrix-Commutative-Ring R n)
+
+  monoid-mul-square-matrix-Commutative-Ring : Monoid l
+  monoid-mul-square-matrix-Commutative-Ring =
+    monoid-mul-unital-associative-algebra-Commutative-Ring
+      ( R)
+      ( unital-associative-algebra-square-matrix-Commutative-Ring)
+
+  ring-square-matrix-Commutative-Ring : Ring l
+  ring-square-matrix-Commutative-Ring =
+    ring-unital-associative-algebra-Commutative-Ring
+      ( R)
+      ( unital-associative-algebra-square-matrix-Commutative-Ring)
+```
diff --git a/src/linear-algebra/constant-grids.lagda.md b/src/linear-algebra/constant-grids.lagda.md
new file mode 100644
index 00000000000..c37831fbf7d
--- /dev/null
+++ b/src/linear-algebra/constant-grids.lagda.md
@@ -0,0 +1,30 @@
+# Constant grids
+
+```agda
+module linear-algebra.constant-grids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.constant-tuples
+open import linear-algebra.grids
+```
+
+</details>
+
+## Idea
+
+Constant grids are [grids](linear-algebra.grids.md) in which all elements are
+the same.
+
+## Definition
+
+```agda
+constant-grid : {l : Level} {A : UU l} {m n : ℕ} → A → grid A m n
+constant-grid a = constant-tuple (constant-tuple a)
+```
diff --git a/src/linear-algebra/constant-matrices.lagda.md b/src/linear-algebra/constant-matrices.lagda.md
deleted file mode 100644
index e939ea23785..00000000000
--- a/src/linear-algebra/constant-matrices.lagda.md
+++ /dev/null
@@ -1,30 +0,0 @@
-# Constant matrices
-
-```agda
-module linear-algebra.constant-matrices where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.universe-levels
-
-open import linear-algebra.constant-tuples
-open import linear-algebra.matrices
-```
-
-</details>
-
-## Idea
-
-Constant matrices are [matrices](linear-algebra.matrices.md) in which all
-elements are the same.
-
-## Definition
-
-```agda
-constant-matrix : {l : Level} {A : UU l} {m n : ℕ} → A → matrix A m n
-constant-matrix a = constant-tuple (constant-tuple a)
-```
diff --git a/src/linear-algebra/diagonal-grids-on-rings.lagda.md b/src/linear-algebra/diagonal-grids-on-rings.lagda.md
new file mode 100644
index 00000000000..1b773befdee
--- /dev/null
+++ b/src/linear-algebra/diagonal-grids-on-rings.lagda.md
@@ -0,0 +1,58 @@
+# Diagonal grids on rings
+
+```agda
+module linear-algebra.diagonal-grids-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.constant-tuples
+open import linear-algebra.grids-on-rings
+open import linear-algebra.tuples-on-rings
+
+open import lists.functoriality-tuples
+open import lists.tuples
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Definitions
+
+A {{#concept "diagonal grid" Agda=diagonal-grid-Ring}} is a
+[grid](linear-algebra.grids-on-rings.md) whose only nonzero elements are on the
+diagonal of the grid.
+
+### Diagonal matrices
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  diagonal-grid-Ring : (n : ℕ) → tuple-Ring R n → grid-Ring R n n
+  diagonal-grid-Ring zero-ℕ v = empty-tuple
+  diagonal-grid-Ring (succ-ℕ n) (x ∷ v) =
+    ( x ∷ zero-tuple-Ring R) ∷
+    ( map-tuple (λ v' → zero-Ring R ∷ v') (diagonal-grid-Ring n v))
+```
+
+### Scalar matrices
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  scalar-grid-Ring : (n : ℕ) → type-Ring R → grid-Ring R n n
+  scalar-grid-Ring n x = diagonal-grid-Ring R n (constant-tuple x)
+
+  identity-grid-Ring : (n : ℕ) → grid-Ring R n n
+  identity-grid-Ring n = scalar-grid-Ring n (one-Ring R)
+```
diff --git a/src/linear-algebra/diagonal-matrices-on-rings.lagda.md b/src/linear-algebra/diagonal-matrices-on-rings.lagda.md
index 45aecbdc7e1..3c95ce9a6df 100644
--- a/src/linear-algebra/diagonal-matrices-on-rings.lagda.md
+++ b/src/linear-algebra/diagonal-matrices-on-rings.lagda.md
@@ -1,6 +1,8 @@
-# Diagonal matrices on rings
+# Diagonal rings on matrices
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module linear-algebra.diagonal-matrices-on-rings where
 ```
 
@@ -9,51 +11,233 @@ module linear-algebra.diagonal-matrices-on-rings where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+open import foundation.coproduct-types
+open import foundation.decidable-propositions
+open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
-open import linear-algebra.constant-tuples
-open import linear-algebra.matrices-on-rings
-open import linear-algebra.tuples-on-rings
-
-open import lists.functoriality-tuples
-open import lists.tuples
+open import linear-algebra.diagonals-of-square-matrices
+open import linear-algebra.finite-sequences-in-rings
+open import linear-algebra.square-matrices-on-rings
+open import linear-algebra.symmetric-matrices
+open import linear-algebra.transposition-matrices
 
 open import ring-theory.rings
+
+open import univalent-combinatorics.equality-standard-finite-types
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
 
-## Definitions
+## Idea
 
 A
-{{#concept "diagonal matrix" Agda=diagonal-matrix-Ring WD="diagonal matrix" WDID=Q332791}}
-is a [matrix](linear-algebra.matrices.md) whose only nonzero elements are on the
-diagonal of the matrix.
+{{#concept "diagonal matrix" Disambiguation="on a ring" WD="diagonal matrix" WDID=Q332791 Agda=diagonal-matrix-Ring}}
+on a [ring](ring-theory.rings.md) is a
+[square matrix](linear-algebra.square-matrices-on-rings.md) `A` where if `i` is
+[not equal to](foundation.negated-equality.md) `j`, then `Aᵢⱼ` is zero.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  is-diagonal-prop-square-matrix-Ring : square-matrix-Ring R n → Prop l
+  is-diagonal-prop-square-matrix-Ring A =
+    Π-Prop
+      ( Fin n)
+      ( λ i →
+        Π-Prop (Fin n) (λ j → nonequal-Prop i j ⇒ is-zero-ring-Prop R (A i j)))
+
+  is-diagonal-square-matrix-Ring : square-matrix-Ring R n → UU l
+  is-diagonal-square-matrix-Ring =
+    is-in-subtype is-diagonal-prop-square-matrix-Ring
 
-### Diagonal matrices
+  diagonal-matrix-Ring : UU l
+  diagonal-matrix-Ring = type-subtype is-diagonal-prop-square-matrix-Ring
+
+  matrix-diagonal-matrix-Ring : diagonal-matrix-Ring → square-matrix-Ring R n
+  matrix-diagonal-matrix-Ring = pr1
+```
+
+### Constructing a diagonal matrix from the finite sequence of elements on the diagonal
 
 ```agda
 module _
-  {l : Level} (R : Ring l)
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
   where
 
-  diagonal-matrix-Ring : (n : ℕ) → tuple-Ring R n → matrix-Ring R n n
-  diagonal-matrix-Ring zero-ℕ v = empty-tuple
-  diagonal-matrix-Ring (succ-ℕ n) (x ∷ v) =
-    ( x ∷ zero-tuple-Ring R) ∷
-    ( map-tuple (λ v' → zero-Ring R ∷ v') (diagonal-matrix-Ring n v))
+  matrix-from-diagonal-fin-sequence-type-Ring :
+    fin-sequence-type-Ring R n → square-matrix-Ring R n
+  matrix-from-diagonal-fin-sequence-type-Ring u i j =
+    rec-coproduct
+      ( λ i=j → u i)
+      ( λ i≠j → zero-Ring R)
+      ( has-decidable-equality-Fin n i j)
 ```
 
-### Scalar matrices
+## Properties
+
+### A matrix constructed from its diagonal is diagonal
 
 ```agda
 module _
-  {l : Level} (R : Ring l)
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
   where
 
-  scalar-matrix-Ring : (n : ℕ) → type-Ring R → matrix-Ring R n n
-  scalar-matrix-Ring n x = diagonal-matrix-Ring R n (constant-tuple x)
+  abstract
+    is-diagonal-matrix-from-diagonal-fin-sequence-type-Ring :
+      (u : fin-sequence-type-Ring R n) →
+      is-diagonal-square-matrix-Ring R n
+        ( matrix-from-diagonal-fin-sequence-type-Ring R n u)
+    is-diagonal-matrix-from-diagonal-fin-sequence-type-Ring u i j i≠j =
+      ap
+        ( rec-coproduct _ _)
+        ( eq-is-prop' (is-prop-is-decidable (is-set-Fin n i j)) _ (inr i≠j))
+
+  diagonal-matrix-fin-sequence-type-Ring :
+    (u : fin-sequence-type-Ring R n) →
+    diagonal-matrix-Ring R n
+  diagonal-matrix-fin-sequence-type-Ring u =
+    ( matrix-from-diagonal-fin-sequence-type-Ring R n u ,
+      is-diagonal-matrix-from-diagonal-fin-sequence-type-Ring u)
+```
+
+### The diagonal of a matrix constructed from its diagonal is the original sequence
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
 
-  identity-matrix-Ring : (n : ℕ) → matrix-Ring R n n
-  identity-matrix-Ring n = scalar-matrix-Ring n (one-Ring R)
+  abstract
+    htpy-diagonal-matrix-from-diagonal-fin-sequence-type-Ring :
+      (u : fin-sequence-type-Ring R n) →
+      diagonal-square-matrix n
+        ( matrix-from-diagonal-fin-sequence-type-Ring R n u) ~
+      u
+    htpy-diagonal-matrix-from-diagonal-fin-sequence-type-Ring u i =
+      ap
+        ( rec-coproduct _ _)
+        ( eq-is-prop' (is-prop-is-decidable (is-set-Fin n i i)) _ (inl refl))
+
+    diagonal-matrix-from-diagonal-fin-sequence-type-Ring :
+      (u : fin-sequence-type-Ring R n) →
+      diagonal-square-matrix n
+        ( matrix-from-diagonal-fin-sequence-type-Ring R n u) ＝
+      u
+    diagonal-matrix-from-diagonal-fin-sequence-type-Ring u =
+      eq-htpy (htpy-diagonal-matrix-from-diagonal-fin-sequence-type-Ring u)
+```
+
+### If a matrix is diagonal, it is equal to the diagonal matrix constructed from its diagonal
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (A : square-matrix-Ring R n)
+  (D : is-diagonal-square-matrix-Ring R n A)
+  where
+
+  abstract
+    htpy-diagonal-matrix-diagonal-square-matrix-Ring :
+      binary-htpy
+        ( matrix-from-diagonal-fin-sequence-type-Ring R n
+          ( diagonal-square-matrix n A))
+        ( A)
+    htpy-diagonal-matrix-diagonal-square-matrix-Ring i j
+      with has-decidable-equality-Fin n i j
+    ... | inl i=j = ap (A i) i=j
+    ... | inr i≠j = inv (D i j i≠j)
+
+    diagonal-matrix-diagonal-square-matrix-Ring :
+      matrix-from-diagonal-fin-sequence-type-Ring R n
+        ( diagonal-square-matrix n A) ＝
+      A
+    diagonal-matrix-diagonal-square-matrix-Ring =
+      eq-binary-htpy _ _ htpy-diagonal-matrix-diagonal-square-matrix-Ring
+```
+
+### The type of diagonal `n × n` matrices is equivalent to the type of finite sequences of length `n`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  is-equiv-matrix-from-diagonal-fin-sequence-type-Ring :
+    is-equiv
+      ( diagonal-matrix-fin-sequence-type-Ring R n)
+  is-equiv-matrix-from-diagonal-fin-sequence-type-Ring =
+    is-equiv-is-invertible
+      ( diagonal-square-matrix n ∘ pr1)
+      ( λ (A , D) →
+        eq-type-subtype
+          ( is-diagonal-prop-square-matrix-Ring R n)
+          ( diagonal-matrix-diagonal-square-matrix-Ring R n A D))
+      ( diagonal-matrix-from-diagonal-fin-sequence-type-Ring R n)
+
+  equiv-diagonal-matrix-fin-sequence-type-Ring :
+    fin-sequence-type-Ring R n ≃ diagonal-matrix-Ring R n
+  equiv-diagonal-matrix-fin-sequence-type-Ring =
+    ( diagonal-matrix-fin-sequence-type-Ring R n ,
+      is-equiv-matrix-from-diagonal-fin-sequence-type-Ring)
+```
+
+### The transposition of a diagonal matrix is the diagonal matrix
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where abstract
+
+  is-symmetric-is-diagonal-square-matrix-Ring :
+    (M : square-matrix-Ring R n) →
+    is-diagonal-square-matrix-Ring R n M → is-symmetric-square-matrix n M
+  is-symmetric-is-diagonal-square-matrix-Ring M H i j
+    with has-decidable-equality-Fin n i j
+  ... | inl i=j =
+    tr (λ k → M k i ＝ M i k) i=j refl
+  ... | inr i≠j =
+    H j i (is-symmetric-nonequal i j i≠j) ∙ inv (H i j i≠j)
+
+  is-symmetric-matrix-from-diagonal-fin-sequence-type-Ring :
+    (d : fin-sequence-type-Ring R n) →
+    is-symmetric-square-matrix n
+      ( matrix-from-diagonal-fin-sequence-type-Ring R n d)
+  is-symmetric-matrix-from-diagonal-fin-sequence-type-Ring d =
+    is-symmetric-is-diagonal-square-matrix-Ring
+      ( matrix-from-diagonal-fin-sequence-type-Ring R n d)
+      ( is-diagonal-matrix-from-diagonal-fin-sequence-type-Ring R n d)
 ```
diff --git a/src/linear-algebra/diagonals-of-square-matrices.lagda.md b/src/linear-algebra/diagonals-of-square-matrices.lagda.md
new file mode 100644
index 00000000000..5d5c55c0c43
--- /dev/null
+++ b/src/linear-algebra/diagonals-of-square-matrices.lagda.md
@@ -0,0 +1,35 @@
+# Diagonals of square matrices
+
+```agda
+module linear-algebra.diagonals-of-square-matrices where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.square-matrices
+
+open import lists.finite-sequences
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "diagonal" Disambiguation="of a square matrix" WD="diagonal of a matrix" WDID=Q77966258 Agda=diagonal-square-matrix}}
+of an `n × n` [square matrix](linear-algebra.square-matrices.md) `A` is the
+[finite sequence](lists.finite-sequences.md) of length `n` defined by
+`dᵢ = Aᵢᵢ`.
+
+## Definition
+
+```agda
+diagonal-square-matrix :
+  {l : Level} {A : UU l} (n : ℕ) → square-matrix A n → fin-sequence A n
+diagonal-square-matrix n A i = A i i
+```
diff --git a/src/linear-algebra/dot-product-finite-sequences-in-commutative-rings.lagda.md b/src/linear-algebra/dot-product-finite-sequences-in-commutative-rings.lagda.md
new file mode 100644
index 00000000000..3bb5f3c9d2a
--- /dev/null
+++ b/src/linear-algebra/dot-product-finite-sequences-in-commutative-rings.lagda.md
@@ -0,0 +1,60 @@
+# The dot product of finite sequences in commutative rings
+
+```agda
+module linear-algebra.dot-product-finite-sequences-in-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.dot-product-finite-sequences-in-rings
+open import linear-algebra.finite-sequences-in-commutative-rings
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "dot product" Disambiguation="of finite sequences in commutative rings" Agda=dot-product-fin-sequence-type-Commutative-Ring}}
+of two
+[finite sequences](linear-algebra.finite-sequences-in-commutative-rings.md) `u`
+and `v` in a [commutative](commutative-algebra.commutative-rings.md) is the
+[sum](commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings.md)
+`∑ᵢ uᵢvᵢ`.
+
+## Definition
+
+```agda
+dot-product-fin-sequence-type-Commutative-Ring :
+  {l : Level} (R : Commutative-Ring l) (n : ℕ) →
+  fin-sequence-type-Commutative-Ring R n →
+  fin-sequence-type-Commutative-Ring R n →
+  type-Commutative-Ring R
+dot-product-fin-sequence-type-Commutative-Ring R =
+  dot-product-fin-sequence-type-Ring (ring-Commutative-Ring R)
+```
+
+## Properties
+
+### The dot product is symmetric
+
+```agda
+abstract
+  symmetric-dot-product-fin-sequence-type-Commutative-Ring :
+    {l : Level} (R : Commutative-Ring l) (n : ℕ)
+    (u v : fin-sequence-type-Commutative-Ring R n) →
+    dot-product-fin-sequence-type-Commutative-Ring R n u v ＝
+    dot-product-fin-sequence-type-Commutative-Ring R n v u
+  symmetric-dot-product-fin-sequence-type-Commutative-Ring R n u v =
+    htpy-sum-fin-sequence-type-Commutative-Ring R n
+      ( λ i → commutative-mul-Commutative-Ring R (u i) (v i))
+```
diff --git a/src/linear-algebra/dot-product-finite-sequences-in-rings.lagda.md b/src/linear-algebra/dot-product-finite-sequences-in-rings.lagda.md
new file mode 100644
index 00000000000..8bc4837c831
--- /dev/null
+++ b/src/linear-algebra/dot-product-finite-sequences-in-rings.lagda.md
@@ -0,0 +1,38 @@
+# The dot product of finite sequences in rings
+
+```agda
+module linear-algebra.dot-product-finite-sequences-in-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.finite-sequences-in-rings
+
+open import ring-theory.rings
+open import ring-theory.sums-of-finite-sequences-of-elements-rings
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "dot product" Disambiguation="of finite sequences in rings" Agda=dot-product-fin-sequence-type-Ring}}
+of two [finite sequences](linear-algebra.finite-sequences-in-rings.md) `u` and
+`v` in a [ring](ring-theory.rings.md) is the
+[sum](ring-theory.sums-of-finite-sequences-of-elements-rings.md) `∑ᵢ uᵢvᵢ`.
+
+## Definition
+
+```agda
+dot-product-fin-sequence-type-Ring :
+  {l : Level} (R : Ring l) (n : ℕ) →
+  fin-sequence-type-Ring R n → fin-sequence-type-Ring R n → type-Ring R
+dot-product-fin-sequence-type-Ring R n u v =
+  sum-fin-sequence-type-Ring R n (λ i → mul-Ring R (u i) (v i))
+```
diff --git a/src/linear-algebra/finite-sequences-in-commutative-rings.lagda.md b/src/linear-algebra/finite-sequences-in-commutative-rings.lagda.md
index bc58a7c70fc..418fc028225 100644
--- a/src/linear-algebra/finite-sequences-in-commutative-rings.lagda.md
+++ b/src/linear-algebra/finite-sequences-in-commutative-rings.lagda.md
@@ -1,6 +1,8 @@
 # Finite sequences in commutative rings
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module linear-algebra.finite-sequences-in-commutative-rings where
 ```
 
@@ -8,19 +10,24 @@ module linear-algebra.finite-sequences-in-commutative-rings where
 
 ```agda
 open import commutative-algebra.commutative-rings
+open import commutative-algebra.function-commutative-rings
 
 open import elementary-number-theory.natural-numbers
 
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels
 
 open import group-theory.abelian-groups
-open import group-theory.commutative-monoids
-open import group-theory.groups
-open import group-theory.monoids
-open import group-theory.semigroups
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
 
 open import linear-algebra.finite-sequences-in-rings
+open import linear-algebra.left-modules-commutative-rings
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-commutative-rings
+
+open import lists.finite-sequences
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -68,6 +75,27 @@ module _
     snoc-fin-sequence-type-Ring (ring-Commutative-Ring R)
 ```
 
+### The left module of finite sequences in a commutative ring
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  where
+
+  left-module-fin-sequence-Commutative-Ring :
+    (n : ℕ) → left-module-Commutative-Ring l R
+  left-module-fin-sequence-Commutative-Ring n =
+    left-module-function-Commutative-Ring R (Fin n)
+
+  scalar-mul-fin-sequence-type-Commutative-Ring :
+    (n : ℕ) →
+    type-Commutative-Ring R → fin-sequence-type-Commutative-Ring R n →
+    fin-sequence-type-Commutative-Ring R n
+  scalar-mul-fin-sequence-type-Commutative-Ring =
+    scalar-mul-fin-sequence-type-Ring
+      ( ring-Commutative-Ring R)
+```
+
 ### The zero finite sequence in a commutative ring
 
 ```agda
@@ -203,24 +231,28 @@ module _
   {l : Level} (R : Commutative-Ring l)
   where
 
-  semigroup-fin-sequence-type-Commutative-Ring : ℕ → Semigroup l
-  semigroup-fin-sequence-type-Commutative-Ring =
-    semigroup-fin-sequence-type-Ring (ring-Commutative-Ring R)
-
-  monoid-fin-sequence-type-Commutative-Ring : ℕ → Monoid l
-  monoid-fin-sequence-type-Commutative-Ring =
-    monoid-fin-sequence-type-Ring (ring-Commutative-Ring R)
-
-  commutative-monoid-fin-sequence-type-Commutative-Ring :
-    ℕ → Commutative-Monoid l
-  commutative-monoid-fin-sequence-type-Commutative-Ring =
-    commutative-monoid-fin-sequence-type-Ring (ring-Commutative-Ring R)
+  ab-fin-sequence-type-Commutative-Ring : ℕ → Ab l
+  ab-fin-sequence-type-Commutative-Ring n =
+    ab-left-module-Commutative-Ring
+      ( R)
+      ( left-module-fin-sequence-Commutative-Ring R n)
+```
 
-  group-fin-sequence-type-Commutative-Ring : ℕ → Group l
-  group-fin-sequence-type-Commutative-Ring =
-    group-fin-sequence-type-Ring (ring-Commutative-Ring R)
+### Coordinates of sequence sums
 
-  ab-fin-sequence-type-Commutative-Ring : ℕ → Ab l
-  ab-fin-sequence-type-Commutative-Ring =
-    ab-fin-sequence-type-Ring (ring-Commutative-Ring R)
+```agda
+abstract
+  coordinate-sum-fin-sequence-fin-sequence-type-Commutative-Ring :
+    {l : Level} (R : Commutative-Ring l) (m n : ℕ) (i : Fin n)
+    (v : fin-sequence (fin-sequence-type-Commutative-Ring R n) m) →
+    sum-fin-sequence-type-left-module-Commutative-Ring
+      ( R)
+      ( left-module-fin-sequence-Commutative-Ring R n)
+      ( m)
+      ( v)
+      ( i) ＝
+    sum-fin-sequence-type-Ab (ab-Commutative-Ring R) m (λ j → v j i)
+  coordinate-sum-fin-sequence-fin-sequence-type-Commutative-Ring R =
+    coordinate-sum-fin-sequence-fin-sequence-type-Ring
+      ( ring-Commutative-Ring R)
 ```
diff --git a/src/linear-algebra/finite-sequences-in-euclidean-domains.lagda.md b/src/linear-algebra/finite-sequences-in-euclidean-domains.lagda.md
index 2731e775d88..60446bf841c 100644
--- a/src/linear-algebra/finite-sequences-in-euclidean-domains.lagda.md
+++ b/src/linear-algebra/finite-sequences-in-euclidean-domains.lagda.md
@@ -21,6 +21,7 @@ open import group-theory.monoids
 open import group-theory.semigroups
 
 open import linear-algebra.finite-sequences-in-commutative-rings
+open import linear-algebra.left-modules-commutative-rings
 
 open import lists.finite-sequences
 open import lists.functoriality-finite-sequences
@@ -207,32 +208,17 @@ module _
       ( commutative-ring-Euclidean-Domain R)
 ```
 
-### The abelian group of pointwise addition
+### The left module of finite sequences on a Euclidean domain
 
 ```agda
 module _
   {l : Level} (R : Euclidean-Domain l)
   where
 
-  semigroup-fin-sequence-type-Euclidean-Domain : ℕ → Semigroup l
-  semigroup-fin-sequence-type-Euclidean-Domain =
-    semigroup-fin-sequence-type-Commutative-Ring
-      ( commutative-ring-Euclidean-Domain R)
-
-  monoid-fin-sequence-type-Euclidean-Domain : ℕ → Monoid l
-  monoid-fin-sequence-type-Euclidean-Domain =
-    monoid-fin-sequence-type-Commutative-Ring
-      ( commutative-ring-Euclidean-Domain R)
-
-  commutative-monoid-fin-sequence-type-Euclidean-Domain :
-    ℕ → Commutative-Monoid l
-  commutative-monoid-fin-sequence-type-Euclidean-Domain =
-    commutative-monoid-fin-sequence-type-Commutative-Ring
-      ( commutative-ring-Euclidean-Domain R)
-
-  group-fin-sequence-type-Euclidean-Domain : ℕ → Group l
-  group-fin-sequence-type-Euclidean-Domain =
-    group-fin-sequence-type-Commutative-Ring
+  left-module-fin-sequence-type-Euclidean-Domain :
+    ℕ → left-module-Commutative-Ring l (commutative-ring-Euclidean-Domain R)
+  left-module-fin-sequence-type-Euclidean-Domain =
+    left-module-fin-sequence-Commutative-Ring
       ( commutative-ring-Euclidean-Domain R)
 
   ab-fin-sequence-type-Euclidean-Domain : ℕ → Ab l
diff --git a/src/linear-algebra/finite-sequences-in-rings.lagda.md b/src/linear-algebra/finite-sequences-in-rings.lagda.md
index 77f9dceacf0..822388f64ce 100644
--- a/src/linear-algebra/finite-sequences-in-rings.lagda.md
+++ b/src/linear-algebra/finite-sequences-in-rings.lagda.md
@@ -9,11 +9,10 @@ module linear-algebra.finite-sequences-in-rings where
 ```agda
 open import elementary-number-theory.natural-numbers
 
-open import foundation.action-on-identifications-binary-functions
 open import foundation.dependent-pair-types
-open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.unit-type
 open import foundation.unital-binary-operations
 open import foundation.universe-levels
 
@@ -22,10 +21,12 @@ open import group-theory.commutative-monoids
 open import group-theory.groups
 open import group-theory.monoids
 open import group-theory.semigroups
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
 
 open import linear-algebra.finite-sequences-in-semirings
 open import linear-algebra.left-modules-rings
 open import linear-algebra.linear-maps-left-modules-rings
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-rings
 
 open import lists.finite-sequences
 open import lists.functoriality-finite-sequences
@@ -75,6 +76,11 @@ module _
 
   fin-sequence-type-Ring : UU l
   fin-sequence-type-Ring = fin-sequence (type-Ring R) n
+
+  scalar-mul-fin-sequence-type-Ring :
+    type-Ring R → fin-sequence-type-Ring → fin-sequence-type-Ring
+  scalar-mul-fin-sequence-type-Ring =
+    mul-left-module-Ring R left-module-fin-sequence-Ring
 ```
 
 ### Inherited algebraic structures on the type of finite sequences in a ring
@@ -312,3 +318,28 @@ module _
     coordinate-map-fin-sequence-Ring ,
     is-linear-coordinate-map-fin-sequence-Ring
 ```
+
+### Coordinates of sequence sums
+
+```agda
+abstract
+  coordinate-sum-fin-sequence-fin-sequence-type-Ring :
+    {l : Level} (R : Ring l) (m n : ℕ) (i : Fin n)
+    (v : fin-sequence (fin-sequence-type-Ring R n) m) →
+    sum-fin-sequence-type-left-module-Ring
+      ( R)
+      ( left-module-fin-sequence-Ring R n)
+      ( m)
+      ( v)
+      ( i) ＝
+    sum-fin-sequence-type-Ab (ab-Ring R) m (λ j → v j i)
+  coordinate-sum-fin-sequence-fin-sequence-type-Ring R m n i =
+    distributive-hom-sum-fin-sequence-type-Ab
+      ( ab-left-module-Ring R (left-module-fin-sequence-Ring R n))
+      ( ab-Ring R)
+      ( hom-ab-linear-map-left-module-Ring R
+        ( left-module-fin-sequence-Ring R n)
+        ( left-module-ring-Ring R)
+        ( coordinate-linear-map-fin-sequence-Ring R n i))
+      ( m)
+```
diff --git a/src/linear-algebra/functoriality-grids.lagda.md b/src/linear-algebra/functoriality-grids.lagda.md
new file mode 100644
index 00000000000..c8568bfe967
--- /dev/null
+++ b/src/linear-algebra/functoriality-grids.lagda.md
@@ -0,0 +1,47 @@
+# Functoriality of the type of grids
+
+```agda
+module linear-algebra.functoriality-grids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.grids
+
+open import lists.functoriality-tuples
+```
+
+</details>
+
+## Idea
+
+Any map `f : A → B` induces a map between [grids](linear-algebra.grids.md)
+`grid A m n → grid B m n`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  map-grid : {m n : ℕ} → grid A m n → grid B m n
+  map-grid = map-tuple (map-tuple f)
+```
+
+### Binary maps
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B → C)
+  where
+
+  binary-map-grid :
+    {m n : ℕ} → grid A m n → grid B m n → grid C m n
+  binary-map-grid = binary-map-tuple (binary-map-tuple f)
+```
diff --git a/src/linear-algebra/functoriality-matrices.lagda.md b/src/linear-algebra/functoriality-matrices.lagda.md
deleted file mode 100644
index 58f07fa963c..00000000000
--- a/src/linear-algebra/functoriality-matrices.lagda.md
+++ /dev/null
@@ -1,47 +0,0 @@
-# Functoriality of the type of matrices
-
-```agda
-module linear-algebra.functoriality-matrices where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.universe-levels
-
-open import linear-algebra.matrices
-
-open import lists.functoriality-tuples
-```
-
-</details>
-
-## Idea
-
-Any map `f : A → B` induces a map between [matrices](linear-algebra.matrices.md)
-`matrix A m n → matrix B m n`.
-
-## Definition
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-  where
-
-  map-matrix : {m n : ℕ} → matrix A m n → matrix B m n
-  map-matrix = map-tuple (map-tuple f)
-```
-
-### Binary maps
-
-```agda
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B → C)
-  where
-
-  binary-map-matrix :
-    {m n : ℕ} → matrix A m n → matrix B m n → matrix C m n
-  binary-map-matrix = binary-map-tuple (binary-map-tuple f)
-```
diff --git a/src/linear-algebra/general-linear-groups-finite-degree-rings.lagda.md b/src/linear-algebra/general-linear-groups-finite-degree-rings.lagda.md
new file mode 100644
index 00000000000..635c9aee07c
--- /dev/null
+++ b/src/linear-algebra/general-linear-groups-finite-degree-rings.lagda.md
@@ -0,0 +1,44 @@
+# The general linear groups of finite degree over rings
+
+```agda
+module linear-algebra.general-linear-groups-finite-degree-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import group-theory.groups
+
+open import linear-algebra.rings-of-square-matrices-on-rings
+
+open import ring-theory.groups-of-units-rings
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "general linear group" Disambiguation="of finite degree over a ring" WDID=Q524607 WD="general linear group" Agda=general-linear-group-Ring}}
+of degree `n : ℕ` over a [ring](ring-theory.rings.md) `R` is the
+[group of units](ring-theory.groups-of-units-rings.md) of the
+[ring of `n × n` square matrices](linear-algebra.rings-of-square-matrices-on-rings.md)
+on `R`.
+
+## Definition
+
+```agda
+general-linear-group-Ring : {l : Level} → ℕ → Ring l → Group l
+general-linear-group-Ring n R =
+  group-of-units-Ring (ring-square-matrix-Ring R n)
+```
+
+## External links
+
+- [General linear group](https://en.wikipedia.org/wiki/General_linear_group) on
+  Wikipedia
diff --git a/src/linear-algebra/grids-on-rings.lagda.md b/src/linear-algebra/grids-on-rings.lagda.md
new file mode 100644
index 00000000000..619be38e954
--- /dev/null
+++ b/src/linear-algebra/grids-on-rings.lagda.md
@@ -0,0 +1,135 @@
+# Grids on rings
+
+```agda
+module linear-algebra.grids-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.constant-grids
+open import linear-algebra.functoriality-grids
+open import linear-algebra.grids
+open import linear-algebra.tuples-on-rings
+
+open import lists.tuples
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Definitions
+
+A [grid](linear-algebra.grids.md) on a [ring](ring-theory.rings.md) is a grid
+whose elements are elements of the ring.
+
+### Grids
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  grid-Ring : ℕ → ℕ → UU l
+  grid-Ring m n = grid (type-Ring R) m n
+```
+
+### The zero grid
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  zero-grid-Ring : {m n : ℕ} → grid-Ring R m n
+  zero-grid-Ring = constant-grid (zero-Ring R)
+```
+
+### Addition of grids on rings
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  add-grid-Ring : {m n : ℕ} (A B : grid-Ring R m n) → grid-Ring R m n
+  add-grid-Ring = binary-map-grid (add-Ring R)
+```
+
+## Properties
+
+### Addition of grids is associative
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  associative-add-grid-Ring :
+    {m n : ℕ} (A B C : grid-Ring R m n) →
+    add-grid-Ring R (add-grid-Ring R A B) C ＝
+    add-grid-Ring R A (add-grid-Ring R B C)
+  associative-add-grid-Ring empty-tuple empty-tuple empty-tuple = refl
+  associative-add-grid-Ring (v ∷ A) (w ∷ B) (z ∷ C) =
+    ap-binary _∷_
+      ( associative-add-tuple-Ring R v w z)
+      ( associative-add-grid-Ring A B C)
+```
+
+### Addition of grids is commutative
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  commutative-add-grid-Ring :
+    {m n : ℕ} (A B : grid-Ring R m n) →
+    add-grid-Ring R A B ＝ add-grid-Ring R B A
+  commutative-add-grid-Ring empty-tuple empty-tuple = refl
+  commutative-add-grid-Ring (v ∷ A) (w ∷ B) =
+    ap-binary _∷_
+      ( commutative-add-tuple-Ring R v w)
+      ( commutative-add-grid-Ring A B)
+```
+
+### Left unit law for addition of grids
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  left-unit-law-add-grid-Ring :
+    {m n : ℕ} (A : grid-Ring R m n) →
+    add-grid-Ring R (zero-grid-Ring R) A ＝ A
+  left-unit-law-add-grid-Ring empty-tuple = refl
+  left-unit-law-add-grid-Ring (v ∷ A) =
+    ap-binary _∷_
+      ( left-unit-law-add-tuple-Ring R v)
+      ( left-unit-law-add-grid-Ring A)
+```
+
+### Right unit law for addition of grids
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  right-unit-law-add-grid-Ring :
+    {m n : ℕ} (A : grid-Ring R m n) →
+    add-grid-Ring R A (zero-grid-Ring R) ＝ A
+  right-unit-law-add-grid-Ring empty-tuple = refl
+  right-unit-law-add-grid-Ring (v ∷ A) =
+    ap-binary _∷_
+      ( right-unit-law-add-tuple-Ring R v)
+      ( right-unit-law-add-grid-Ring A)
+```
diff --git a/src/linear-algebra/grids.lagda.md b/src/linear-algebra/grids.lagda.md
new file mode 100644
index 00000000000..e510c19b233
--- /dev/null
+++ b/src/linear-algebra/grids.lagda.md
@@ -0,0 +1,116 @@
+# Grids
+
+```agda
+module linear-algebra.grids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import lists.functoriality-tuples
+open import lists.tuples
+```
+
+</details>
+
+## Idea
+
+An `m × n` {{#concept "grid" Agda=grid}} of elements in `A` is a
+[tuple](lists.tuples.md) of length `m` of tuples of length `n` of elements of
+`A`. In other words, a grid is an arrangement of elements of `A` with `m` rows
+and `n` columns.
+
+## Definitions
+
+### Grids
+
+```agda
+grid : {l : Level} (A : UU l) → ℕ → ℕ → UU l
+grid A m n = tuple (tuple A n) m
+```
+
+### The top row of a grid
+
+```agda
+top-row-grid :
+  {l : Level} {m n : ℕ} {A : UU l} → grid A (succ-ℕ m) n → tuple A n
+top-row-grid (v ∷ M) = v
+```
+
+### The left column of a grid
+
+```agda
+left-column-grid :
+  {l : Level} {m n : ℕ} {A : UU l} → grid A m (succ-ℕ n) → tuple A m
+left-column-grid = map-tuple head-tuple
+```
+
+### The vertical tail of a grid
+
+```agda
+vertical-tail-grid :
+  {l : Level} {m n : ℕ} {A : UU l} → grid A (succ-ℕ m) n → grid A m n
+vertical-tail-grid M = tail-tuple M
+```
+
+### The horizontal tail of a grid
+
+```agda
+horizontal-tail-grid :
+  {l : Level} {m n : ℕ} {A : UU l} → grid A m (succ-ℕ n) → grid A m n
+horizontal-tail-grid = map-tuple tail-tuple
+```
+
+### The vertically empty grid
+
+```agda
+vertically-empty-grid :
+  {l : Level} {n : ℕ} {A : UU l} → grid A 0 n
+vertically-empty-grid = empty-tuple
+
+eq-vertically-empty-grid :
+  {l : Level} {n : ℕ} {A : UU l}
+  (x : grid A 0 n) → vertically-empty-grid ＝ x
+eq-vertically-empty-grid empty-tuple = refl
+
+is-contr-grid-zero-ℕ :
+  {l : Level} {n : ℕ} {A : UU l} → is-contr (grid A 0 n)
+pr1 is-contr-grid-zero-ℕ = vertically-empty-grid
+pr2 is-contr-grid-zero-ℕ = eq-vertically-empty-grid
+```
+
+### The horizontally empty grid
+
+```agda
+horizontally-empty-grid :
+  {l : Level} {m : ℕ} {A : UU l} → grid A m 0
+horizontally-empty-grid {m = zero-ℕ} = empty-tuple
+horizontally-empty-grid {m = succ-ℕ m} =
+  empty-tuple ∷ horizontally-empty-grid
+
+eq-horizontally-empty-grid :
+  {l : Level} {m : ℕ} {A : UU l}
+  (x : grid A m 0) → horizontally-empty-grid ＝ x
+eq-horizontally-empty-grid {m = zero-ℕ} empty-tuple = refl
+eq-horizontally-empty-grid {m = succ-ℕ m} (empty-tuple ∷ M) =
+  ap-binary _∷_ refl (eq-horizontally-empty-grid M)
+
+is-contr-grid-zero-ℕ' :
+  {l : Level} {m : ℕ} {A : UU l} → is-contr (grid A m 0)
+pr1 is-contr-grid-zero-ℕ' = horizontally-empty-grid
+pr2 is-contr-grid-zero-ℕ' = eq-horizontally-empty-grid
+```
+
+## See also
+
+- [Matrices](linear-algebra.matrices.md), the analogous concept but with
+  [finite sequences](lists.finite-sequences.md) in the role of
+  [tuples](lists.tuples.md)
diff --git a/src/linear-algebra/identity-matrices-on-commutative-rings.lagda.md b/src/linear-algebra/identity-matrices-on-commutative-rings.lagda.md
new file mode 100644
index 00000000000..93a42c473da
--- /dev/null
+++ b/src/linear-algebra/identity-matrices-on-commutative-rings.lagda.md
@@ -0,0 +1,41 @@
+# Identity matrices on commutative rings
+
+```agda
+module linear-algebra.identity-matrices-on-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.identity-matrices-on-rings
+open import linear-algebra.square-matrices-on-commutative-rings
+```
+
+</details>
+
+## Idea
+
+The `n × n`
+{{#concept "identity matrix" Disambiguation="on a commutative ring" WDID=Q193794 WD="identity matrix" Agda=id-matrix-Commutative-Ring}}
+on a [commutative ring](commutative-algebra.commutative-rings.md) is the
+[diagonal matrix](linear-algebra.diagonal-matrices-on-rings.md) with all 1s on
+the diagonal.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  id-matrix-Commutative-Ring : square-matrix-Commutative-Ring R n
+  id-matrix-Commutative-Ring = id-matrix-Ring (ring-Commutative-Ring R) n
+```
diff --git a/src/linear-algebra/identity-matrices-on-rings.lagda.md b/src/linear-algebra/identity-matrices-on-rings.lagda.md
new file mode 100644
index 00000000000..8a50b1c18ab
--- /dev/null
+++ b/src/linear-algebra/identity-matrices-on-rings.lagda.md
@@ -0,0 +1,42 @@
+# Identity matrices on rings
+
+```agda
+module linear-algebra.identity-matrices-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.diagonal-matrices-on-rings
+open import linear-algebra.square-matrices-on-rings
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+The `n × n`
+{{#concept "identity matrix" Disambiguation="on a ring" WDID=Q193794 WD="identity matrix" Agda=id-matrix-Ring}}
+on a [ring](ring-theory.rings.md) is the
+[diagonal matrix](linear-algebra.diagonal-matrices-on-rings.md) with all 1s on
+the diagonal.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  id-matrix-Ring : square-matrix-Ring R n
+  id-matrix-Ring =
+    matrix-from-diagonal-fin-sequence-type-Ring R n (λ _ → one-Ring R)
+```
diff --git a/src/linear-algebra/indicator-finite-sequences-in-commutative-rings.lagda.md b/src/linear-algebra/indicator-finite-sequences-in-commutative-rings.lagda.md
new file mode 100644
index 00000000000..b3aa57f1efe
--- /dev/null
+++ b/src/linear-algebra/indicator-finite-sequences-in-commutative-rings.lagda.md
@@ -0,0 +1,165 @@
+# Indicator finite sequences in commutative rings
+
+```agda
+module linear-algebra.indicator-finite-sequences-in-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.universe-levels
+
+open import linear-algebra.dot-product-finite-sequences-in-commutative-rings
+open import linear-algebra.finite-sequences-in-commutative-rings
+open import linear-algebra.indicator-finite-sequences-in-rings
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-commutative-rings
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "indicator finite sequence" Disambiguation="in a commutative ring" Agda=indicator-fin-sequence-type-Commutative-Ring}}
+in a [commutative ring](commutative-algebra.commutative-rings.md) `R` `χᵢ` for
+index `i : Fin n` is a
+[finite sequence](linear-algebra.finite-sequences-in-commutative-rings.md) in
+`R` `u` such that `uᵢ = 1` and `uⱼ = 0` whenever `j ≠ i`.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  (i : Fin n)
+  where
+
+  indicator-fin-sequence-type-Commutative-Ring :
+    fin-sequence-type-Commutative-Ring R n
+  indicator-fin-sequence-type-Commutative-Ring =
+    indicator-fin-sequence-type-Ring (ring-Commutative-Ring R) n i
+
+  abstract
+    compute-at-index-indicator-fin-sequence-type-Commutative-Ring :
+      indicator-fin-sequence-type-Commutative-Ring i ＝ one-Commutative-Ring R
+    compute-at-index-indicator-fin-sequence-type-Commutative-Ring =
+      compute-at-index-indicator-fin-sequence-type-Ring
+        ( ring-Commutative-Ring R)
+        ( n)
+        ( i)
+
+    compute-at-other-index-indicator-fin-sequence-type-Commutative-Ring :
+      (j : Fin n) → i ≠ j →
+      indicator-fin-sequence-type-Commutative-Ring j ＝ zero-Commutative-Ring R
+    compute-at-other-index-indicator-fin-sequence-type-Commutative-Ring =
+      compute-at-other-index-indicator-fin-sequence-type-Ring
+        ( ring-Commutative-Ring R)
+        ( n)
+        ( i)
+```
+
+## Properties
+
+### `χᵢⱼ = χⱼᵢ`
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where abstract
+
+  symmetric-indicator-fin-sequence-type-Commutative-Ring :
+    (i j : Fin n) →
+    indicator-fin-sequence-type-Commutative-Ring R n i j ＝
+    indicator-fin-sequence-type-Commutative-Ring R n j i
+  symmetric-indicator-fin-sequence-type-Commutative-Ring =
+    symmetric-indicator-fin-sequence-type-Ring (ring-Commutative-Ring R) n
+```
+
+### The dot product of an indicator sequence for index `i` with a finite sequence `v` is `v i`
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  (i : Fin n)
+  where abstract
+
+  left-dot-product-indicator-fin-sequence-type-Commutative-Ring :
+    (u : fin-sequence-type-Commutative-Ring R n) →
+    dot-product-fin-sequence-type-Commutative-Ring R n
+      ( indicator-fin-sequence-type-Commutative-Ring R n i)
+      ( u) ＝
+    u i
+  left-dot-product-indicator-fin-sequence-type-Commutative-Ring =
+    left-dot-product-indicator-fin-sequence-type-Ring
+      ( ring-Commutative-Ring R)
+      ( n)
+      ( i)
+
+  right-dot-product-indicator-fin-sequence-type-Commutative-Ring :
+    (u : fin-sequence-type-Commutative-Ring R n) →
+    dot-product-fin-sequence-type-Commutative-Ring R n
+      ( u)
+      ( indicator-fin-sequence-type-Commutative-Ring R n i) ＝
+    u i
+  right-dot-product-indicator-fin-sequence-type-Commutative-Ring =
+    right-dot-product-indicator-fin-sequence-type-Ring
+      ( ring-Commutative-Ring R)
+      ( n)
+      ( i)
+```
+
+### Every finite sequence in a commutative ring is a linear combination of indicator sequences
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  (v : fin-sequence-type-Commutative-Ring R n)
+  where abstract
+
+  htpy-linear-combination-indicator-fin-sequence-type-Commutative-Ring :
+    sum-fin-sequence-type-left-module-Commutative-Ring
+      ( R)
+      ( left-module-fin-sequence-Commutative-Ring R n)
+      ( n)
+      ( λ i →
+        scalar-mul-fin-sequence-type-Commutative-Ring R n
+          ( v i)
+          ( indicator-fin-sequence-type-Commutative-Ring R n i)) ~
+    v
+  htpy-linear-combination-indicator-fin-sequence-type-Commutative-Ring =
+    htpy-linear-combination-indicator-fin-sequence-type-Ring
+      ( ring-Commutative-Ring R)
+      ( n)
+      ( v)
+
+  eq-linear-combination-indicator-fin-sequence-type-Commutative-Ring :
+    sum-fin-sequence-type-left-module-Commutative-Ring
+      ( R)
+      ( left-module-fin-sequence-Commutative-Ring R n)
+      ( n)
+      ( λ i →
+        scalar-mul-fin-sequence-type-Commutative-Ring R n
+          ( v i)
+          ( indicator-fin-sequence-type-Commutative-Ring R n i)) ＝
+    v
+  eq-linear-combination-indicator-fin-sequence-type-Commutative-Ring =
+    eq-htpy htpy-linear-combination-indicator-fin-sequence-type-Commutative-Ring
+```
diff --git a/src/linear-algebra/indicator-finite-sequences-in-rings.lagda.md b/src/linear-algebra/indicator-finite-sequences-in-rings.lagda.md
new file mode 100644
index 00000000000..b0b91f807d3
--- /dev/null
+++ b/src/linear-algebra/indicator-finite-sequences-in-rings.lagda.md
@@ -0,0 +1,318 @@
+# Indicator finite sequences in rings
+
+```agda
+module linear-algebra.indicator-finite-sequences-in-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.decidable-propositions
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.propositions
+open import foundation.singleton-subtypes-discrete-types
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
+
+open import linear-algebra.dot-product-finite-sequences-in-rings
+open import linear-algebra.finite-sequences-in-rings
+open import linear-algebra.sums-of-finite-sequences-of-elements-left-modules-rings
+
+open import ring-theory.central-elements-rings
+open import ring-theory.rings
+open import ring-theory.sums-of-finite-families-of-elements-rings
+open import ring-theory.sums-of-finite-sequences-of-elements-rings
+
+open import univalent-combinatorics.counting
+open import univalent-combinatorics.decidable-subtypes
+open import univalent-combinatorics.equality-standard-finite-types
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "indicator finite sequence" Disambiguation="in a ring" Agda=indicator-fin-sequence-type-Ring}}
+in a [ring](ring-theory.rings.md) `R` `χᵢ` for index `i : Fin n` is a
+[finite sequence](linear-algebra.finite-sequences-in-rings.md) in `R` `u` such
+that `uᵢ = 1` and `uⱼ = 0` whenever `j ≠ i`.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  indicator-fin-sequence-type-Ring :
+    (i : Fin n) → fin-sequence-type-Ring R n
+  indicator-fin-sequence-type-Ring i j =
+    rec-coproduct
+      ( λ _ → one-Ring R)
+      ( λ _ → zero-Ring R)
+      ( has-decidable-equality-Fin n i j)
+
+  abstract
+    compute-at-index-indicator-fin-sequence-type-Ring :
+      (i : Fin n) → indicator-fin-sequence-type-Ring i i ＝ one-Ring R
+    compute-at-index-indicator-fin-sequence-type-Ring i =
+      ap
+        ( rec-coproduct (λ _ → one-Ring R) (λ _ → zero-Ring R))
+        ( eq-is-prop'
+          ( is-prop-is-decidable (is-set-Fin n i i))
+          ( has-decidable-equality-Fin n i i)
+          ( inl refl))
+
+    compute-at-other-index-indicator-fin-sequence-type-Ring :
+      (i j : Fin n) → i ≠ j →
+      indicator-fin-sequence-type-Ring i j ＝ zero-Ring R
+    compute-at-other-index-indicator-fin-sequence-type-Ring i j i≠j =
+      ap
+        ( rec-coproduct (λ _ → one-Ring R) (λ _ → zero-Ring R))
+        ( eq-is-prop'
+          ( is-prop-is-decidable (is-set-Fin n i j))
+          ( has-decidable-equality-Fin n i j)
+          ( inr i≠j))
+```
+
+## Properties
+
+### `χᵢⱼ = χⱼᵢ`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where abstract
+
+  symmetric-indicator-fin-sequence-type-Ring :
+    (i j : Fin n) →
+    indicator-fin-sequence-type-Ring R n i j ＝
+    indicator-fin-sequence-type-Ring R n j i
+  symmetric-indicator-fin-sequence-type-Ring i j
+    with has-decidable-equality-Fin n i j
+  ... | inl i=j =
+    ap
+      ( rec-coproduct (λ _ → one-Ring R) (λ _ → zero-Ring R))
+      ( eq-is-prop'
+        ( is-prop-is-decidable (is-set-Fin n j i))
+        ( inl (inv i=j))
+        ( has-decidable-equality-Fin n j i))
+  ... | inr i≠j =
+    ap
+      ( rec-coproduct (λ _ → one-Ring R) (λ _ → zero-Ring R))
+      ( eq-is-prop'
+        ( is-prop-is-decidable (is-set-Fin n j i))
+        ( inr (is-symmetric-nonequal i j i≠j))
+        ( has-decidable-equality-Fin n j i))
+```
+
+### Every coordinate of an indicator sequence at an index `i` is central
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (i : Fin n)
+  where abstract
+
+  is-central-element-indicator-fin-sequence-type-Ring :
+    (j : Fin n) →
+    is-central-element-Ring R (indicator-fin-sequence-type-Ring R n i j)
+  is-central-element-indicator-fin-sequence-type-Ring j
+    with has-decidable-equality-Fin n i j
+  ... | inl i=j = is-central-element-one-Ring R
+  ... | inr i≠j = is-central-element-zero-Ring R
+```
+
+### The dot product of an indicator sequence for index `i` with a finite sequence `v` is `v i`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (i : Fin n)
+  where abstract
+
+  left-dot-product-indicator-fin-sequence-type-Ring :
+    (u : fin-sequence-type-Ring R n) →
+    dot-product-fin-sequence-type-Ring R n
+      ( indicator-fin-sequence-type-Ring R n i)
+      ( u) ＝
+    u i
+  left-dot-product-indicator-fin-sequence-type-Ring u =
+    equational-reasoning
+      dot-product-fin-sequence-type-Ring R n
+        ( indicator-fin-sequence-type-Ring R n i)
+        ( u)
+      ＝
+        sum-finite-Ab
+          ( ab-Ring R)
+          ( Fin-Finite-Type n)
+          ( λ j → mul-Ring R (indicator-fin-sequence-type-Ring R n i j) (u j))
+        by
+          inv
+            ( eq-sum-finite-sum-count-Ab
+              ( ab-Ring R)
+              ( Fin-Finite-Type n)
+              ( count-Fin n)
+              ( _))
+      ＝
+        sum-finite-Ab
+          ( ab-Ring R)
+          ( finite-type-subset-Finite-Type
+            ( Fin-Finite-Type n)
+            ( decidable-standard-singleton-subtype-Discrete-Type
+              ( Fin-Discrete-Type n)
+              ( i)))
+          ( λ (j , _) →
+            mul-Ring R (indicator-fin-sequence-type-Ring R n i j) (u j))
+        by
+          vanish-sum-complement-decidable-subset-finite-Ab
+            ( ab-Ring R)
+            ( Fin-Finite-Type n)
+            ( decidable-standard-singleton-subtype-Discrete-Type
+              ( Fin-Discrete-Type n)
+              ( i))
+            ( _)
+            ( λ j j≠i →
+              equational-reasoning
+                mul-Ring R (indicator-fin-sequence-type-Ring R n i j) (u j)
+                ＝ mul-Ring R (zero-Ring R) (u j)
+                  by
+                    ap-mul-Ring R
+                      ( compute-at-other-index-indicator-fin-sequence-type-Ring
+                        ( R)
+                        ( n)
+                        ( i)
+                        ( j)
+                        ( is-symmetric-nonequal j i j≠i))
+                      ( refl)
+                ＝ zero-Ring R
+                  by left-zero-law-mul-Ring R (u j))
+      ＝ mul-Ring R (indicator-fin-sequence-type-Ring R n i i) (u i)
+        by
+          sum-finite-is-contr-Ab
+            ( ab-Ring R)
+            ( _)
+            ( is-contr-type-decidable-standard-singleton-subtype-Discrete-Type
+              ( Fin-Discrete-Type n)
+              ( i))
+            ( i , refl)
+            ( _)
+      ＝ mul-Ring R (one-Ring R) (u i)
+        by
+          ap-mul-Ring R
+            ( compute-at-index-indicator-fin-sequence-type-Ring R n i)
+            ( refl)
+      ＝ u i
+        by left-unit-law-mul-Ring R (u i)
+
+  right-dot-product-indicator-fin-sequence-type-Ring :
+    (u : fin-sequence-type-Ring R n) →
+    dot-product-fin-sequence-type-Ring R n
+      ( u)
+      ( indicator-fin-sequence-type-Ring R n i) ＝
+    u i
+  right-dot-product-indicator-fin-sequence-type-Ring u =
+    ( htpy-sum-fin-sequence-type-Ring R n
+      ( λ j →
+        inv
+          ( is-central-element-indicator-fin-sequence-type-Ring
+            ( R)
+            ( n)
+            ( i)
+            ( j)
+            ( u j)))) ∙
+    ( left-dot-product-indicator-fin-sequence-type-Ring u)
+```
+
+### Every finite sequence in a ring is a linear combination of indicator sequences
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (v : fin-sequence-type-Ring R n)
+  where abstract
+
+  htpy-linear-combination-indicator-fin-sequence-type-Ring :
+    sum-fin-sequence-type-left-module-Ring
+      ( R)
+      ( left-module-fin-sequence-Ring R n)
+      ( n)
+      ( λ i →
+        scalar-mul-fin-sequence-type-Ring R n
+          ( v i)
+          ( indicator-fin-sequence-type-Ring R n i)) ~
+    v
+  htpy-linear-combination-indicator-fin-sequence-type-Ring k =
+    equational-reasoning
+      sum-fin-sequence-type-left-module-Ring R
+        ( left-module-fin-sequence-Ring R n) n
+        ( λ i →
+          scalar-mul-fin-sequence-type-Ring R n
+            ( v i)
+            ( indicator-fin-sequence-type-Ring R n i))
+        ( k)
+      ＝
+        sum-fin-sequence-type-Ring
+          ( R)
+          ( n)
+          ( λ j →
+            mul-Ring
+              ( R)
+              ( v j)
+              ( indicator-fin-sequence-type-Ring R n j k))
+        by coordinate-sum-fin-sequence-fin-sequence-type-Ring R n n k _
+      ＝
+        sum-fin-sequence-type-Ring
+          ( R)
+          ( n)
+          ( λ j →
+            mul-Ring
+              ( R)
+              ( v j)
+              ( indicator-fin-sequence-type-Ring R n k j))
+        by
+          htpy-sum-fin-sequence-type-Ring R n
+            ( λ j →
+              ap-mul-Ring R
+                ( refl)
+                ( symmetric-indicator-fin-sequence-type-Ring R n j k))
+      ＝ v k
+        by right-dot-product-indicator-fin-sequence-type-Ring R n k v
+
+  eq-linear-combination-indicator-fin-sequence-type-Ring :
+    sum-fin-sequence-type-left-module-Ring
+      ( R)
+      ( left-module-fin-sequence-Ring R n)
+      ( n)
+      ( λ i →
+        scalar-mul-fin-sequence-type-Ring R n
+          ( v i)
+          ( indicator-fin-sequence-type-Ring R n i)) ＝
+    v
+  eq-linear-combination-indicator-fin-sequence-type-Ring =
+    eq-htpy htpy-linear-combination-indicator-fin-sequence-type-Ring
+```
diff --git a/src/linear-algebra/matrices-on-commutative-rings.lagda.md b/src/linear-algebra/matrices-on-commutative-rings.lagda.md
new file mode 100644
index 00000000000..961f86b46f1
--- /dev/null
+++ b/src/linear-algebra/matrices-on-commutative-rings.lagda.md
@@ -0,0 +1,168 @@
+# Matrices on commutative rings
+
+```agda
+module linear-algebra.matrices-on-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import linear-algebra.left-modules-commutative-rings
+open import linear-algebra.matrices-on-rings
+```
+
+</details>
+
+## Idea
+
+A [matrix](linear-algebra.matrices.md) on a
+[commutative ring](commutative-algebra.commutative-rings.md) is a matrix whose
+elements are elements of the ring.
+
+## Definition
+
+```agda
+matrix-Commutative-Ring : {l : Level} → Commutative-Ring l → ℕ → ℕ → UU l
+matrix-Commutative-Ring R = matrix-Ring (ring-Commutative-Ring R)
+```
+
+## Properties
+
+### Matrices on a commutative ring form a left module over that ring
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (m n : ℕ)
+  where
+
+  left-module-matrix-Commutative-Ring : left-module-Commutative-Ring l R
+  left-module-matrix-Commutative-Ring =
+    left-module-matrix-Ring (ring-Commutative-Ring R) m n
+
+  set-matrix-Commutative-Ring : Set l
+  set-matrix-Commutative-Ring =
+    set-left-module-Commutative-Ring R left-module-matrix-Commutative-Ring
+
+  add-matrix-Commutative-Ring :
+    matrix-Commutative-Ring R m n → matrix-Commutative-Ring R m n →
+    matrix-Commutative-Ring R m n
+  add-matrix-Commutative-Ring =
+    add-left-module-Commutative-Ring R left-module-matrix-Commutative-Ring
+
+  zero-matrix-Commutative-Ring : matrix-Commutative-Ring R m n
+  zero-matrix-Commutative-Ring =
+    zero-left-module-Commutative-Ring R left-module-matrix-Commutative-Ring
+
+  left-unit-law-add-matrix-Commutative-Ring :
+    (A : matrix-Commutative-Ring R m n) →
+    add-matrix-Commutative-Ring zero-matrix-Commutative-Ring A ＝ A
+  left-unit-law-add-matrix-Commutative-Ring =
+    left-unit-law-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  right-unit-law-add-matrix-Commutative-Ring :
+    (A : matrix-Commutative-Ring R m n) →
+    add-matrix-Commutative-Ring A zero-matrix-Commutative-Ring ＝ A
+  right-unit-law-add-matrix-Commutative-Ring =
+    right-unit-law-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  associative-add-matrix-Commutative-Ring :
+    (A B C : matrix-Commutative-Ring R m n) →
+    add-matrix-Commutative-Ring (add-matrix-Commutative-Ring A B) C ＝
+    add-matrix-Commutative-Ring A (add-matrix-Commutative-Ring B C)
+  associative-add-matrix-Commutative-Ring =
+    associative-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  commutative-add-matrix-Commutative-Ring :
+    (A B : matrix-Commutative-Ring R m n) →
+    add-matrix-Commutative-Ring A B ＝ add-matrix-Commutative-Ring B A
+  commutative-add-matrix-Commutative-Ring =
+    commutative-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  neg-matrix-Commutative-Ring :
+    matrix-Commutative-Ring R m n → matrix-Commutative-Ring R m n
+  neg-matrix-Commutative-Ring =
+    neg-left-module-Commutative-Ring R left-module-matrix-Commutative-Ring
+
+  left-inverse-law-add-matrix-Commutative-Ring :
+    (A : matrix-Commutative-Ring R m n) →
+    add-matrix-Commutative-Ring (neg-matrix-Commutative-Ring A) A ＝
+    zero-matrix-Commutative-Ring
+  left-inverse-law-add-matrix-Commutative-Ring =
+    left-inverse-law-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  right-inverse-law-add-matrix-Commutative-Ring :
+    (A : matrix-Commutative-Ring R m n) →
+    add-matrix-Commutative-Ring A (neg-matrix-Commutative-Ring A) ＝
+    zero-matrix-Commutative-Ring
+  right-inverse-law-add-matrix-Commutative-Ring =
+    right-inverse-law-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  scalar-mul-matrix-Commutative-Ring :
+    type-Commutative-Ring R → matrix-Commutative-Ring R m n →
+    matrix-Commutative-Ring R m n
+  scalar-mul-matrix-Commutative-Ring =
+    mul-left-module-Commutative-Ring R left-module-matrix-Commutative-Ring
+
+  left-unit-law-scalar-mul-matrix-Commutative-Ring :
+    (A : matrix-Commutative-Ring R m n) →
+    scalar-mul-matrix-Commutative-Ring (one-Commutative-Ring R) A ＝ A
+  left-unit-law-scalar-mul-matrix-Commutative-Ring =
+    left-unit-law-mul-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  associative-scalar-mul-matrix-Commutative-Ring :
+    (r s : type-Commutative-Ring R) (A : matrix-Commutative-Ring R m n) →
+    scalar-mul-matrix-Commutative-Ring (mul-Commutative-Ring R r s) A ＝
+    scalar-mul-matrix-Commutative-Ring
+      ( r)
+      ( scalar-mul-matrix-Commutative-Ring s A)
+  associative-scalar-mul-matrix-Commutative-Ring =
+    associative-mul-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  left-distributive-scalar-mul-add-matrix-Commutative-Ring :
+    (r : type-Commutative-Ring R) (A B : matrix-Commutative-Ring R m n) →
+    scalar-mul-matrix-Commutative-Ring r (add-matrix-Commutative-Ring A B) ＝
+    add-matrix-Commutative-Ring
+      ( scalar-mul-matrix-Commutative-Ring r A)
+      ( scalar-mul-matrix-Commutative-Ring r B)
+  left-distributive-scalar-mul-add-matrix-Commutative-Ring =
+    left-distributive-mul-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+
+  right-distributive-scalar-mul-add-matrix-Commutative-Ring :
+    (r s : type-Commutative-Ring R) (A : matrix-Commutative-Ring R m n) →
+    scalar-mul-matrix-Commutative-Ring (add-Commutative-Ring R r s) A ＝
+    add-matrix-Commutative-Ring
+      ( scalar-mul-matrix-Commutative-Ring r A)
+      ( scalar-mul-matrix-Commutative-Ring s A)
+  right-distributive-scalar-mul-add-matrix-Commutative-Ring =
+    right-distributive-mul-add-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring)
+```
diff --git a/src/linear-algebra/matrices-on-rings.lagda.md b/src/linear-algebra/matrices-on-rings.lagda.md
index dc0b7373112..1b726285dfb 100644
--- a/src/linear-algebra/matrices-on-rings.lagda.md
+++ b/src/linear-algebra/matrices-on-rings.lagda.md
@@ -9,127 +9,132 @@ module linear-algebra.matrices-on-rings where
 ```agda
 open import elementary-number-theory.natural-numbers
 
-open import foundation.action-on-identifications-binary-functions
 open import foundation.identity-types
+open import foundation.sets
 open import foundation.universe-levels
 
-open import linear-algebra.constant-matrices
-open import linear-algebra.functoriality-matrices
-open import linear-algebra.matrices
-open import linear-algebra.tuples-on-rings
+open import group-theory.abelian-groups
 
-open import lists.tuples
+open import linear-algebra.finite-sequences-in-rings
+open import linear-algebra.function-left-modules-rings
+open import linear-algebra.left-modules-rings
+open import linear-algebra.matrices
 
 open import ring-theory.rings
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
 
-## Definitions
+## Idea
 
 A [matrix](linear-algebra.matrices.md) on a [ring](ring-theory.rings.md) is a
 matrix whose elements are elements of the ring.
 
-### Matrices
-
-```agda
-module _
-  {l : Level} (R : Ring l)
-  where
-
-  matrix-Ring : ℕ → ℕ → UU l
-  matrix-Ring m n = matrix (type-Ring R) m n
-```
-
-### The zero matrix
+## Definition
 
 ```agda
-module _
-  {l : Level} (R : Ring l)
-  where
-
-  zero-matrix-Ring : {m n : ℕ} → matrix-Ring R m n
-  zero-matrix-Ring = constant-matrix (zero-Ring R)
-```
-
-### Addition of matrices on rings
-
-```agda
-module _
-  {l : Level} (R : Ring l)
-  where
-
-  add-matrix-Ring : {m n : ℕ} (A B : matrix-Ring R m n) → matrix-Ring R m n
-  add-matrix-Ring = binary-map-matrix (add-Ring R)
+matrix-Ring : {l : Level} → Ring l → ℕ → ℕ → UU l
+matrix-Ring R = matrix (type-Ring R)
 ```
 
 ## Properties
 
-### Addition of matrices is associative
+### Matrices on a ring form a left module over that ring
 
 ```agda
 module _
-  {l : Level} (R : Ring l)
+  {l : Level}
+  (R : Ring l)
+  (m n : ℕ)
   where
 
-  associative-add-matrix-Ring :
-    {m n : ℕ} (A B C : matrix-Ring R m n) →
-    add-matrix-Ring R (add-matrix-Ring R A B) C ＝
-    add-matrix-Ring R A (add-matrix-Ring R B C)
-  associative-add-matrix-Ring empty-tuple empty-tuple empty-tuple = refl
-  associative-add-matrix-Ring (v ∷ A) (w ∷ B) (z ∷ C) =
-    ap-binary _∷_
-      ( associative-add-tuple-Ring R v w z)
-      ( associative-add-matrix-Ring A B C)
-```
+  left-module-matrix-Ring : left-module-Ring l R
+  left-module-matrix-Ring =
+    function-left-module-Ring
+      ( R)
+      ( function-left-module-ring-Ring R (Fin n))
+      ( Fin m)
 
-### Addition of matrices is commutative
+  set-matrix-Ring : Set l
+  set-matrix-Ring = set-left-module-Ring R left-module-matrix-Ring
 
-```agda
-module _
-  {l : Level} (R : Ring l)
-  where
+  ab-matrix-Ring : Ab l
+  ab-matrix-Ring = ab-left-module-Ring R left-module-matrix-Ring
 
-  commutative-add-matrix-Ring :
-    {m n : ℕ} (A B : matrix-Ring R m n) →
-    add-matrix-Ring R A B ＝ add-matrix-Ring R B A
-  commutative-add-matrix-Ring empty-tuple empty-tuple = refl
-  commutative-add-matrix-Ring (v ∷ A) (w ∷ B) =
-    ap-binary _∷_
-      ( commutative-add-tuple-Ring R v w)
-      ( commutative-add-matrix-Ring A B)
-```
+  add-matrix-Ring : matrix-Ring R m n → matrix-Ring R m n → matrix-Ring R m n
+  add-matrix-Ring = add-left-module-Ring R left-module-matrix-Ring
 
-### Left unit law for addition of matrices
-
-```agda
-module _
-  {l : Level} (R : Ring l)
-  where
+  zero-matrix-Ring : matrix-Ring R m n
+  zero-matrix-Ring = zero-left-module-Ring R left-module-matrix-Ring
 
   left-unit-law-add-matrix-Ring :
-    {m n : ℕ} (A : matrix-Ring R m n) →
-    add-matrix-Ring R (zero-matrix-Ring R) A ＝ A
-  left-unit-law-add-matrix-Ring empty-tuple = refl
-  left-unit-law-add-matrix-Ring (v ∷ A) =
-    ap-binary _∷_
-      ( left-unit-law-add-tuple-Ring R v)
-      ( left-unit-law-add-matrix-Ring A)
-```
+    (A : matrix-Ring R m n) → add-matrix-Ring zero-matrix-Ring A ＝ A
+  left-unit-law-add-matrix-Ring =
+    left-unit-law-add-left-module-Ring R left-module-matrix-Ring
 
-### Right unit law for addition of matrices
+  right-unit-law-add-matrix-Ring :
+    (A : matrix-Ring R m n) → add-matrix-Ring A zero-matrix-Ring ＝ A
+  right-unit-law-add-matrix-Ring =
+    right-unit-law-add-left-module-Ring R left-module-matrix-Ring
 
-```agda
-module _
-  {l : Level} (R : Ring l)
-  where
+  associative-add-matrix-Ring :
+    (A B C : matrix-Ring R m n) →
+    add-matrix-Ring (add-matrix-Ring A B) C ＝
+    add-matrix-Ring A (add-matrix-Ring B C)
+  associative-add-matrix-Ring =
+    associative-add-left-module-Ring R left-module-matrix-Ring
 
-  right-unit-law-add-matrix-Ring :
-    {m n : ℕ} (A : matrix-Ring R m n) →
-    add-matrix-Ring R A (zero-matrix-Ring R) ＝ A
-  right-unit-law-add-matrix-Ring empty-tuple = refl
-  right-unit-law-add-matrix-Ring (v ∷ A) =
-    ap-binary _∷_
-      ( right-unit-law-add-tuple-Ring R v)
-      ( right-unit-law-add-matrix-Ring A)
+  commutative-add-matrix-Ring :
+    (A B : matrix-Ring R m n) →
+    add-matrix-Ring A B ＝ add-matrix-Ring B A
+  commutative-add-matrix-Ring =
+    commutative-add-left-module-Ring R left-module-matrix-Ring
+
+  neg-matrix-Ring : matrix-Ring R m n → matrix-Ring R m n
+  neg-matrix-Ring = neg-left-module-Ring R left-module-matrix-Ring
+
+  left-inverse-law-add-matrix-Ring :
+    (A : matrix-Ring R m n) →
+    add-matrix-Ring (neg-matrix-Ring A) A ＝ zero-matrix-Ring
+  left-inverse-law-add-matrix-Ring =
+    left-inverse-law-add-left-module-Ring R left-module-matrix-Ring
+
+  right-inverse-law-add-matrix-Ring :
+    (A : matrix-Ring R m n) →
+    add-matrix-Ring A (neg-matrix-Ring A) ＝ zero-matrix-Ring
+  right-inverse-law-add-matrix-Ring =
+    right-inverse-law-add-left-module-Ring R left-module-matrix-Ring
+
+  scalar-mul-matrix-Ring : type-Ring R → matrix-Ring R m n → matrix-Ring R m n
+  scalar-mul-matrix-Ring =
+    mul-left-module-Ring R left-module-matrix-Ring
+
+  left-unit-law-scalar-mul-matrix-Ring :
+    (A : matrix-Ring R m n) →
+    scalar-mul-matrix-Ring (one-Ring R) A ＝ A
+  left-unit-law-scalar-mul-matrix-Ring =
+    left-unit-law-mul-left-module-Ring R left-module-matrix-Ring
+
+  associative-scalar-mul-matrix-Ring :
+    (r s : type-Ring R) (A : matrix-Ring R m n) →
+    scalar-mul-matrix-Ring (mul-Ring R r s) A ＝
+    scalar-mul-matrix-Ring r (scalar-mul-matrix-Ring s A)
+  associative-scalar-mul-matrix-Ring =
+    associative-mul-left-module-Ring R left-module-matrix-Ring
+
+  left-distributive-scalar-mul-add-matrix-Ring :
+    (r : type-Ring R) (A B : matrix-Ring R m n) →
+    scalar-mul-matrix-Ring r (add-matrix-Ring A B) ＝
+    add-matrix-Ring (scalar-mul-matrix-Ring r A) (scalar-mul-matrix-Ring r B)
+  left-distributive-scalar-mul-add-matrix-Ring =
+    left-distributive-mul-add-left-module-Ring R left-module-matrix-Ring
+
+  right-distributive-scalar-mul-add-matrix-Ring :
+    (r s : type-Ring R) (A : matrix-Ring R m n) →
+    scalar-mul-matrix-Ring (add-Ring R r s) A ＝
+    add-matrix-Ring (scalar-mul-matrix-Ring r A) (scalar-mul-matrix-Ring s A)
+  right-distributive-scalar-mul-add-matrix-Ring =
+    right-distributive-mul-add-left-module-Ring R left-module-matrix-Ring
 ```
diff --git a/src/linear-algebra/matrices.lagda.md b/src/linear-algebra/matrices.lagda.md
index cbc676603e2..82fa4a0a996 100644
--- a/src/linear-algebra/matrices.lagda.md
+++ b/src/linear-algebra/matrices.lagda.md
@@ -9,15 +9,17 @@ module linear-algebra.matrices where
 ```agda
 open import elementary-number-theory.natural-numbers
 
-open import foundation.action-on-identifications-binary-functions
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
-open import foundation.dependent-products-contractible-types
-open import foundation.identity-types
+open import foundation.dependent-products-truncated-types
+open import foundation.function-types
+open import foundation.sets
+open import foundation.truncated-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
-open import lists.functoriality-tuples
-open import lists.tuples
+open import lists.finite-sequences
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -25,87 +27,143 @@ open import lists.tuples
 ## Idea
 
 An `m × n` {{#concept "matrix" Agda=matrix WD="matrix" WDID=Q44337}} of elements
-in `A` is an arrangement of elements of A with `m` rows and `n` columns. In
-other words, a matrix is a [tuple](lists.tuples.md) of length `m` of tuples of
-length `n` of elements of `A`.
-
-## Definitions
+in `A` is a [finite sequence](lists.finite-sequences.md) of length `m` of finite
+sequences of length `n` in `A`.
 
-### Matrices
+## Definition
 
 ```agda
 matrix : {l : Level} (A : UU l) → ℕ → ℕ → UU l
-matrix A m n = tuple (tuple A n) m
+matrix A m n = fin-sequence (fin-sequence A n) m
 ```
 
+## Properties
+
 ### The top row of a matrix
 
 ```agda
-top-row-matrix :
-  {l : Level} {m n : ℕ} {A : UU l} → matrix A (succ-ℕ m) n → tuple A n
-top-row-matrix (v ∷ M) = v
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  top-row-matrix : matrix A (succ-ℕ m) n → fin-sequence A n
+  top-row-matrix = head-fin-sequence m
 ```
 
-### The left column of a matrix
+### The vertical tail of a matrix
 
 ```agda
-left-column-matrix :
-  {l : Level} {m n : ℕ} {A : UU l} → matrix A m (succ-ℕ n) → tuple A m
-left-column-matrix = map-tuple head-tuple
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  vertical-tail-matrix : matrix A (succ-ℕ m) n → matrix A m n
+  vertical-tail-matrix = tail-fin-sequence m
 ```
 
-### The vertical tail of a matrix
+### The bottom row of a matrix
 
 ```agda
-vertical-tail-matrix :
-  {l : Level} {m n : ℕ} {A : UU l} → matrix A (succ-ℕ m) n → matrix A m n
-vertical-tail-matrix M = tail-tuple M
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  bottom-row-matrix : matrix A (succ-ℕ m) n → fin-sequence A n
+  bottom-row-matrix M = last-fin-sequence m M
+```
+
+### The vertical initial segment of a matrix
+
+```agda
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  vertical-init-matrix : matrix A (succ-ℕ m) n → matrix A m n
+  vertical-init-matrix M = init-fin-sequence m M
+```
+
+### The first column of a matrix
+
+```agda
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  first-column-matrix : matrix A m (succ-ℕ n) → fin-sequence A m
+  first-column-matrix M = head-fin-sequence n ∘ M
 ```
 
 ### The horizontal tail of a matrix
 
 ```agda
-horizontal-tail-matrix :
-  {l : Level} {m n : ℕ} {A : UU l} → matrix A m (succ-ℕ n) → matrix A m n
-horizontal-tail-matrix = map-tuple tail-tuple
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  horizontal-tail-matrix : matrix A m (succ-ℕ n) → matrix A m n
+  horizontal-tail-matrix M = tail-fin-sequence n ∘ M
 ```
 
-### The vertically empty matrix
+### The last column of a matrix
 
 ```agda
-vertically-empty-matrix :
-  {l : Level} {n : ℕ} {A : UU l} → matrix A 0 n
-vertically-empty-matrix = empty-tuple
-
-eq-vertically-empty-matrix :
-  {l : Level} {n : ℕ} {A : UU l}
-  (x : matrix A 0 n) → vertically-empty-matrix ＝ x
-eq-vertically-empty-matrix empty-tuple = refl
-
-is-contr-matrix-zero-ℕ :
-  {l : Level} {n : ℕ} {A : UU l} → is-contr (matrix A 0 n)
-pr1 is-contr-matrix-zero-ℕ = vertically-empty-matrix
-pr2 is-contr-matrix-zero-ℕ = eq-vertically-empty-matrix
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  last-column-matrix : matrix A m (succ-ℕ n) → fin-sequence A m
+  last-column-matrix M = last-fin-sequence n ∘ M
 ```
 
-### The horizontally empty matrix
+### The horizontal initial segment of a matrix
 
 ```agda
-horizontally-empty-matrix :
-  {l : Level} {m : ℕ} {A : UU l} → matrix A m 0
-horizontally-empty-matrix {m = zero-ℕ} = empty-tuple
-horizontally-empty-matrix {m = succ-ℕ m} =
-  empty-tuple ∷ horizontally-empty-matrix
-
-eq-horizontally-empty-matrix :
-  {l : Level} {m : ℕ} {A : UU l}
-  (x : matrix A m 0) → horizontally-empty-matrix ＝ x
-eq-horizontally-empty-matrix {m = zero-ℕ} empty-tuple = refl
-eq-horizontally-empty-matrix {m = succ-ℕ m} (empty-tuple ∷ M) =
-  ap-binary _∷_ refl (eq-horizontally-empty-matrix M)
-
-is-contr-matrix-zero-ℕ' :
-  {l : Level} {m : ℕ} {A : UU l} → is-contr (matrix A m 0)
-pr1 is-contr-matrix-zero-ℕ' = horizontally-empty-matrix
-pr2 is-contr-matrix-zero-ℕ' = eq-horizontally-empty-matrix
+module _
+  {l : Level}
+  {A : UU l}
+  (m n : ℕ)
+  where
+
+  horizontal-init-matrix : matrix A m (succ-ℕ n) → matrix A m n
+  horizontal-init-matrix M = init-fin-sequence n ∘ M
 ```
+
+### Truncation of matrix types
+
+```agda
+abstract
+  is-trunc-matrix :
+    (k : 𝕋) {l : Level} {A : UU l} (m n : ℕ) →
+    is-trunc k A →
+    is-trunc k (matrix A m n)
+  is-trunc-matrix k m n tA =
+    is-trunc-function-type k (is-trunc-function-type k tA)
+
+matrix-Set : {l : Level} → Set l → ℕ → ℕ → Set l
+matrix-Set (A , is-set-A) m n =
+  ( matrix A m n ,
+    is-trunc-matrix zero-𝕋 m n is-set-A)
+```
+
+## See also
+
+- [Grids](linear-algebra.grids.md), the analogous concept but with
+  [tuples](lists.tuples.md) in the role of
+  [finite sequences](lists.finite-sequences.md)
+- [Square matrices](linear-algebra.square-matrices.md)
+- [Matrices on rings](linear-algebra.matrices-on-rings.md)
diff --git a/src/linear-algebra/multiplication-diagonal-matrices-rings.lagda.md b/src/linear-algebra/multiplication-diagonal-matrices-rings.lagda.md
new file mode 100644
index 00000000000..bfef9a1e0c8
--- /dev/null
+++ b/src/linear-algebra/multiplication-diagonal-matrices-rings.lagda.md
@@ -0,0 +1,209 @@
+# Multiplication by diagonal matrices over rings
+
+```agda
+module linear-algebra.multiplication-diagonal-matrices-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-homotopies
+open import foundation.coproduct-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.diagonal-matrices-on-rings
+open import linear-algebra.finite-sequences-in-rings
+open import linear-algebra.indicator-finite-sequences-in-rings
+open import linear-algebra.matrices-on-rings
+open import linear-algebra.multiplication-matrices-on-rings
+open import linear-algebra.transposition-matrices
+
+open import ring-theory.rings
+open import ring-theory.sums-of-finite-sequences-of-elements-rings
+
+open import univalent-combinatorics.equality-standard-finite-types
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+Given a [diagonal matrix](linear-algebra.diagonal-matrices-on-rings.md) `M` on a
+[ring](ring-theory.rings.md) `R` with diagonal `d`, `MN` is `N` with row `i`
+multiplied by `dᵢ`, and `NM` is `N` with column `j` multiplied by `dⱼ`.
+
+## Properties
+
+### The row at index `i` of a diagonal matrix with diagonal `d` is `dᵢ * χᵢ`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (d : fin-sequence-type-Ring R n)
+  where abstract
+
+  htpy-row-matrix-from-diagonal-fin-sequence-type-Ring :
+    (i : Fin n) →
+    matrix-from-diagonal-fin-sequence-type-Ring R n d i ~
+    scalar-mul-fin-sequence-type-Ring R n
+      ( d i)
+      ( indicator-fin-sequence-type-Ring R n i)
+  htpy-row-matrix-from-diagonal-fin-sequence-type-Ring i j
+    with has-decidable-equality-Fin n i j
+  ... | inl i=j =
+    inv (right-unit-law-mul-Ring R (d i))
+  ... | inr i≠j =
+    inv (right-zero-law-mul-Ring R (d i))
+```
+
+### Left multiplication by a diagonal matrix with diagonal `d` multiplies row `i` by `dᵢ`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n : ℕ)
+  (d : fin-sequence-type-Ring R m)
+  where abstract
+
+  compute-left-mul-diagonal-matrix-Ring :
+    (M : matrix-Ring R m n) (i : Fin m) (j : Fin n) →
+    mul-matrix-Ring R m m n
+      ( matrix-from-diagonal-fin-sequence-type-Ring R m d)
+      ( M)
+      ( i)
+      ( j) ＝
+    mul-Ring R (d i) (M i j)
+  compute-left-mul-diagonal-matrix-Ring M i j =
+    equational-reasoning
+      sum-fin-sequence-type-Ring R m
+        ( λ k →
+          mul-Ring R
+            ( matrix-from-diagonal-fin-sequence-type-Ring R m d i k)
+            ( M k j))
+      ＝
+        sum-fin-sequence-type-Ring R m
+          ( λ k →
+            mul-Ring R
+              ( mul-Ring R
+                ( d i)
+                ( indicator-fin-sequence-type-Ring R m i k))
+              ( M k j))
+        by
+          htpy-sum-fin-sequence-type-Ring R m
+            ( λ k →
+              ap-mul-Ring R
+                ( htpy-row-matrix-from-diagonal-fin-sequence-type-Ring R
+                  ( m)
+                  ( d)
+                  ( i)
+                  ( k))
+                ( refl))
+      ＝
+        sum-fin-sequence-type-Ring R m
+          ( λ k →
+            mul-Ring R
+              ( d i)
+              ( mul-Ring R
+                ( indicator-fin-sequence-type-Ring R m i k)
+                ( M k j)))
+        by
+          htpy-sum-fin-sequence-type-Ring R m
+            ( λ k → associative-mul-Ring R _ _ _)
+      ＝
+        mul-Ring R
+          ( d i)
+          ( sum-fin-sequence-type-Ring R m
+            ( λ k →
+              mul-Ring R
+                ( indicator-fin-sequence-type-Ring R m i k)
+                ( M k j)))
+        by inv (left-distributive-mul-sum-fin-sequence-type-Ring R m _ _)
+      ＝ mul-Ring R (d i) (M i j)
+        by
+          ap-mul-Ring R
+            ( refl)
+            ( left-dot-product-indicator-fin-sequence-type-Ring R m i
+              ( transpose-matrix m n M j))
+```
+
+### Right multiplication by a diagonal matrix with diagonal `d` multiplies column `j` by `dⱼ`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n : ℕ)
+  (d : fin-sequence-type-Ring R n)
+  where abstract
+
+  compute-right-mul-diagonal-matrix-Ring :
+    (M : matrix-Ring R m n) (i : Fin m) (j : Fin n) →
+    mul-matrix-Ring R m n n
+      ( M)
+      ( matrix-from-diagonal-fin-sequence-type-Ring R n d)
+      ( i)
+      ( j) ＝
+    mul-Ring R (M i j) (d j)
+  compute-right-mul-diagonal-matrix-Ring M i j =
+    equational-reasoning
+      sum-fin-sequence-type-Ring R n
+        ( λ k →
+          mul-Ring R
+            ( M i k)
+            ( matrix-from-diagonal-fin-sequence-type-Ring R n d k j))
+      ＝
+        sum-fin-sequence-type-Ring R n
+          ( λ k →
+            mul-Ring R
+              ( M i k)
+              ( matrix-from-diagonal-fin-sequence-type-Ring R n d j k))
+        by
+          htpy-sum-fin-sequence-type-Ring R n
+            ( λ k →
+              ap-mul-Ring R
+                ( refl)
+                ( is-symmetric-matrix-from-diagonal-fin-sequence-type-Ring
+                  ( R)
+                  ( n)
+                  ( d)
+                  ( j)
+                  ( k)))
+      ＝
+        sum-fin-sequence-type-Ring R n
+          ( λ k →
+            mul-Ring R
+              ( M i k)
+              ( mul-Ring R
+                ( d j)
+                ( indicator-fin-sequence-type-Ring R n j k)))
+        by
+          htpy-sum-fin-sequence-type-Ring R n
+            ( λ k →
+              ap-mul-Ring R
+                ( refl)
+                ( htpy-row-matrix-from-diagonal-fin-sequence-type-Ring
+                  ( R)
+                  ( n)
+                  ( d)
+                  ( j)
+                  ( k)))
+      ＝
+        sum-fin-sequence-type-Ring R n
+          ( λ k →
+            mul-Ring R
+              ( mul-Ring R (M i k) (d j))
+              ( indicator-fin-sequence-type-Ring R n j k))
+        by
+          htpy-sum-fin-sequence-type-Ring R n
+            ( λ k → inv (associative-mul-Ring R _ _ _))
+      ＝ mul-Ring R (M i j) (d j)
+        by right-dot-product-indicator-fin-sequence-type-Ring R n j _
+```
diff --git a/src/linear-algebra/multiplication-matrices.lagda.md b/src/linear-algebra/multiplication-grids.lagda.md
similarity index 77%
rename from src/linear-algebra/multiplication-matrices.lagda.md
rename to src/linear-algebra/multiplication-grids.lagda.md
index 7d30a008b07..e65cb32f541 100644
--- a/src/linear-algebra/multiplication-matrices.lagda.md
+++ b/src/linear-algebra/multiplication-grids.lagda.md
@@ -1,7 +1,7 @@
-# Multiplication of matrices
+# Multiplication of grids
 
 ```agda
-module linear-algebra.multiplication-matrices where
+module linear-algebra.multiplication-grids where
 ```
 
 <details><summary>Imports</summary>
@@ -14,24 +14,24 @@ module linear-algebra.multiplication-matrices where
 
 ## Definition
 
-### Multiplication of matrices
+### Multiplication of grids
 
 ```agda
 {-
-mul-tuple-matrix : {l : Level} → {K : UU l} → {m n : ℕ} →
+mul-tuple-grid : {l : Level} → {K : UU l} → {m n : ℕ} →
                      (K → K → K) → (K → K → K) → K →
                      tuple K m → Mat K m n → tuple K n
-mul-tuple-matrix _ _ zero empty-tuple empty-tuple = diagonal-product zero
-mul-tuple-matrix mulK addK zero (x ∷ xs) (v ∷ vs) =
+mul-tuple-grid _ _ zero empty-tuple empty-tuple = diagonal-product zero
+mul-tuple-grid mulK addK zero (x ∷ xs) (v ∷ vs) =
   add-tuple addK (mul-scalar-tuple mulK x v)
-               (mul-tuple-matrix mulK addK zero xs vs)
+               (mul-tuple-grid mulK addK zero xs vs)
 
 mul-Mat : {l' : Level} → {K : UU l'} → {l m n : ℕ} →
           (K → K → K) → (K → K → K) → K →
           Mat K l m → Mat K m n → Mat K l n
 mul-Mat _ _ zero empty-tuple _ = empty-tuple
 mul-Mat mulK addK zero (v ∷ vs) m =
-  mul-tuple-matrix mulK addK zero v m
+  mul-tuple-grid mulK addK zero v m
     ∷ mul-Mat mulK addK zero vs m
 -}
 ```
@@ -52,7 +52,7 @@ mul-transpose mulK-comm (a ∷ as) b = {!!}
 -}
 ```
 
-## Properties of Matrix Multiplication
+## Properties of Grid Multiplication
 
 - distributive laws (incomplete)
 - associativity (TODO)
@@ -68,7 +68,7 @@ module _
   {zero : K}
   where
 
-  left-distributive-tuple-matrix :
+  left-distributive-tuple-grid :
     {n m : ℕ} →
     ( {l : ℕ} →
       diagonal-product {n = l} zero ＝
@@ -77,23 +77,23 @@ module _
     ((x y : K) → addK x y ＝ addK y x) →
     ((x y z : K) → addK x (addK y z) ＝ addK (addK x y) z) →
     (a : tuple K n) (b : Mat K n m) (c : Mat K n m) →
-    ( mul-tuple-matrix mulK addK zero a (add-Mat addK b c)) ＝
+    ( mul-tuple-grid mulK addK zero a (add-Mat addK b c)) ＝
     ( add-tuple
         ( addK)
-        ( mul-tuple-matrix mulK addK zero a b)
-        ( mul-tuple-matrix mulK addK zero a c))
-  left-distributive-tuple-matrix id-tuple _ _ _ empty-tuple empty-tuple empty-tuple =
+        ( mul-tuple-grid mulK addK zero a b)
+        ( mul-tuple-grid mulK addK zero a c))
+  left-distributive-tuple-grid id-tuple _ _ _ empty-tuple empty-tuple empty-tuple =
     id-tuple
-  left-distributive-tuple-matrix
+  left-distributive-tuple-grid
     id-tuple k-distr addK-comm addK-associative (a ∷ as) (r1 ∷ r1s) (r2 ∷ r2s) =
       ap
         ( λ r →
           add-tuple addK r
-            (mul-tuple-matrix mulK addK zero as (add-Mat addK r1s r2s)))
+            (mul-tuple-grid mulK addK zero as (add-Mat addK r1s r2s)))
         (left-distributive-scalar-tuple {zero = zero} k-distr a r1 r2)
         ∙ (ap (λ r → add-tuple addK (add-tuple addK (map-tuple (mulK a) r1)
                                   (mul-scalar-tuple mulK a r2)) r)
-              (left-distributive-tuple-matrix
+              (left-distributive-tuple-grid
                 id-tuple k-distr addK-comm addK-associative as r1s r2s)
           ∙ lemma-shuffle)
     where
@@ -118,7 +118,7 @@ module _
         ∙ commutative-add-tuples
             {zero = zero} addK-comm (add-tuple addK y w) (add-tuple addK x z)))))))
 
-  left-distributive-matrices :
+  left-distributive-grids :
     {n m p : ℕ} →
     ({l : ℕ} →
       diagonal-product {n = l} zero ＝
@@ -129,19 +129,19 @@ module _
     (a : Mat K m n) (b : Mat K n p) (c : Mat K n p) →
     ( mul-Mat mulK addK zero a (add-Mat addK b c)) ＝
     ( add-Mat addK (mul-Mat mulK addK zero a b) (mul-Mat mulK addK zero a c))
-  left-distributive-matrices _ _ _ _ empty-tuple _ _ = refl
-  left-distributive-matrices id-tuple k-distr addK-comm addK-associative (a ∷ as) b c =
+  left-distributive-grids _ _ _ _ empty-tuple _ _ = refl
+  left-distributive-grids id-tuple k-distr addK-comm addK-associative (a ∷ as) b c =
     (ap (λ r → r ∷ mul-Mat mulK addK zero as (add-Mat addK b c))
-        (left-distributive-tuple-matrix
+        (left-distributive-tuple-grid
           id-tuple k-distr addK-comm addK-associative a b c))
-      ∙ ap (_∷_ (add-tuple addK (mul-tuple-matrix mulK addK zero a b)
-                              (mul-tuple-matrix mulK addK zero a c)))
-          (left-distributive-matrices
+      ∙ ap (_∷_ (add-tuple addK (mul-tuple-grid mulK addK zero a b)
+                              (mul-tuple-grid mulK addK zero a c)))
+          (left-distributive-grids
             id-tuple k-distr addK-comm addK-associative as b c)
 -}
 
 {- TODO: right distributivity
-  right-distributive-matrices :
+  right-distributive-grids :
     {n m p : ℕ} →
     ({l : ℕ} →
       diagonal-product {n = l} zero ＝
@@ -152,23 +152,23 @@ module _
     (b : Mat K n p) (c : Mat K n p) (d : Mat K p m) →
     mul-Mat mulK addK zero (add-Mat addK b c) d ＝
     add-Mat addK (mul-Mat mulK addK zero b d) (mul-Mat mulK addK zero c d)
-  right-distributive-matrices _ _ _ _ empty-tuple empty-tuple _ = refl
-  right-distributive-matrices
+  right-distributive-grids _ _ _ _ empty-tuple empty-tuple _ = refl
+  right-distributive-grids
     {p = .zero-ℕ}
     id-tuple k-distr addK-comm addK-associative (b ∷ bs) (c ∷ cs) empty-tuple =
     {!!}
-  right-distributive-matrices
+  right-distributive-grids
     id-tuple k-distr addK-comm addK-associative (b ∷ bs) (c ∷ cs) (d ∷ ds) =
     {!!}
   -- this might also need a proof that zero is the additive identity
 
   TODO: associativity
-  associative-mul-matrices :
+  associative-mul-grids :
     {l : Level} {K : UU l} {n m p q : ℕ} →
     {addK : K → K → K} {mulK : K → K → K} {zero : K} →
     (x : Mat K m n) → (y : Mat K n p) → (z : Mat K p q) →
     mul-Mat mulK addK zero x (mul-Mat mulK addK zero y z) ＝
     mul-Mat mulK addK zero (mul-Mat mulK addK zero x y) z
-  associative-mul-matrices x y z = {!!}
+  associative-mul-grids x y z = {!!}
 -}
 ```
diff --git a/src/linear-algebra/multiplication-matrices-on-commutative-rings.lagda.md b/src/linear-algebra/multiplication-matrices-on-commutative-rings.lagda.md
new file mode 100644
index 00000000000..430661cbf04
--- /dev/null
+++ b/src/linear-algebra/multiplication-matrices-on-commutative-rings.lagda.md
@@ -0,0 +1,225 @@
+# Multiplication of matrices on commutative rings
+
+```agda
+module linear-algebra.multiplication-matrices-on-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-homotopies
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.bilinear-maps-left-modules-commutative-rings
+open import linear-algebra.matrices-on-commutative-rings
+open import linear-algebra.multiplication-matrices-on-rings
+```
+
+</details>
+
+## Idea
+
+[Matrix multiplication](linear-algebra.multiplication-matrices-on-rings.md) on
+[commutative rings](commutative-algebra.commutative-rings.md) is a
+[bilinear map](linear-algebra.bilinear-maps-left-modules-commutative-rings.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (m n p : ℕ)
+  where
+
+  mul-matrix-Commutative-Ring :
+    matrix-Commutative-Ring R m n → matrix-Commutative-Ring R n p →
+    matrix-Commutative-Ring R m p
+  mul-matrix-Commutative-Ring =
+    mul-matrix-Ring (ring-Commutative-Ring R) m n p
+```
+
+## Properties
+
+### Multiplication of matrices is associative
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  where
+
+  abstract
+    associative-mul-matrix-Commutative-Ring :
+      (m n p q : ℕ)
+      (A : matrix-Commutative-Ring R m n)
+      (B : matrix-Commutative-Ring R n p)
+      (C : matrix-Commutative-Ring R p q) →
+      mul-matrix-Commutative-Ring R m p q
+        ( mul-matrix-Commutative-Ring R m n p A B)
+        ( C) ＝
+      mul-matrix-Commutative-Ring R m n q
+        ( A)
+        ( mul-matrix-Commutative-Ring R n p q B C)
+    associative-mul-matrix-Commutative-Ring =
+      associative-mul-matrix-Ring (ring-Commutative-Ring R)
+```
+
+### Multiplication of matrices is distributive over addition
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (m n p : ℕ)
+  where
+
+  abstract
+    left-distributive-mul-add-matrix-Commutative-Ring :
+      (A : matrix-Commutative-Ring R m n)
+      (B C : matrix-Commutative-Ring R n p) →
+      mul-matrix-Commutative-Ring R m n p
+        ( A)
+        ( add-matrix-Commutative-Ring R n p B C) ＝
+      add-matrix-Commutative-Ring R m p
+        ( mul-matrix-Commutative-Ring R m n p A B)
+        ( mul-matrix-Commutative-Ring R m n p A C)
+    left-distributive-mul-add-matrix-Commutative-Ring =
+      left-distributive-mul-add-matrix-Ring (ring-Commutative-Ring R) m n p
+
+    right-distributive-mul-add-matrix-Commutative-Ring :
+      (A B : matrix-Commutative-Ring R m n)
+      (C : matrix-Commutative-Ring R n p) →
+      mul-matrix-Commutative-Ring R m n p
+        ( add-matrix-Commutative-Ring R m n A B)
+        ( C) ＝
+      add-matrix-Commutative-Ring R m p
+        ( mul-matrix-Commutative-Ring R m n p A C)
+        ( mul-matrix-Commutative-Ring R m n p B C)
+    right-distributive-mul-add-matrix-Commutative-Ring =
+      right-distributive-mul-add-matrix-Ring (ring-Commutative-Ring R) m n p
+```
+
+### `(rA)B = r(AB)`
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (m n p : ℕ)
+  where
+
+  abstract
+    associative-scalar-mul-mul-matrix-Commutative-Ring :
+      (r : type-Commutative-Ring R)
+      (A : matrix-Commutative-Ring R m n)
+      (B : matrix-Commutative-Ring R n p) →
+      mul-matrix-Commutative-Ring R m n p
+        ( scalar-mul-matrix-Commutative-Ring R m n r A)
+        ( B) ＝
+      scalar-mul-matrix-Commutative-Ring R m p
+        ( r)
+        ( mul-matrix-Commutative-Ring R m n p A B)
+    associative-scalar-mul-mul-matrix-Commutative-Ring =
+      associative-scalar-mul-mul-matrix-Ring (ring-Commutative-Ring R) m n p
+```
+
+### `A(rB) = r(AB)`
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (m n p : ℕ)
+  (A : matrix-Commutative-Ring R m n)
+  (r : type-Commutative-Ring R)
+  (B : matrix-Commutative-Ring R n p)
+  where
+
+  abstract
+    htpy-left-swap-mul-scalar-mul-matrix-Ring :
+      binary-htpy
+        ( mul-matrix-Commutative-Ring R m n p
+          ( A)
+          ( scalar-mul-matrix-Commutative-Ring R n p r B))
+        ( scalar-mul-matrix-Commutative-Ring R m p
+          ( r)
+          ( mul-matrix-Commutative-Ring R m n p A B))
+    htpy-left-swap-mul-scalar-mul-matrix-Ring i k =
+      ( htpy-sum-fin-sequence-type-Commutative-Ring R n
+        ( λ j → left-swap-mul-Commutative-Ring R (A i j) r (B j k))) ∙
+      ( inv
+        ( left-distributive-mul-sum-fin-sequence-type-Commutative-Ring R n r _))
+
+    left-swap-mul-scalar-mul-matrix-Ring :
+      mul-matrix-Commutative-Ring R m n p
+        ( A)
+        ( scalar-mul-matrix-Commutative-Ring R n p r B) ＝
+      scalar-mul-matrix-Commutative-Ring R m p
+        ( r)
+        ( mul-matrix-Commutative-Ring R m n p A B)
+    left-swap-mul-scalar-mul-matrix-Ring =
+      eq-binary-htpy _ _ htpy-left-swap-mul-scalar-mul-matrix-Ring
+```
+
+### Matrix multiplication is a bilinear map
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (m n p : ℕ)
+  where
+
+  is-linear-on-left-mul-matrix-Commutative-Ring :
+    is-linear-on-left-binary-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring R m n)
+      ( left-module-matrix-Commutative-Ring R n p)
+      ( left-module-matrix-Commutative-Ring R m p)
+      ( mul-matrix-Commutative-Ring R m n p)
+  is-linear-on-left-mul-matrix-Commutative-Ring B =
+    ( ( λ A A' →
+        right-distributive-mul-add-matrix-Commutative-Ring R m n p A A' B) ,
+      ( λ r A →
+        associative-scalar-mul-mul-matrix-Commutative-Ring R m n p r A B))
+
+  is-linear-on-right-mul-matrix-Commutative-Ring :
+    is-linear-on-right-binary-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring R m n)
+      ( left-module-matrix-Commutative-Ring R n p)
+      ( left-module-matrix-Commutative-Ring R m p)
+      ( mul-matrix-Commutative-Ring R m n p)
+  is-linear-on-right-mul-matrix-Commutative-Ring A =
+    ( left-distributive-mul-add-matrix-Commutative-Ring R m n p A ,
+      left-swap-mul-scalar-mul-matrix-Ring R m n p A)
+
+  is-bilinear-map-mul-matrix-Commutative-Ring :
+    is-bilinear-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring R m n)
+      ( left-module-matrix-Commutative-Ring R n p)
+      ( left-module-matrix-Commutative-Ring R m p)
+      ( mul-matrix-Commutative-Ring R m n p)
+  is-bilinear-map-mul-matrix-Commutative-Ring =
+    ( is-linear-on-left-mul-matrix-Commutative-Ring ,
+      is-linear-on-right-mul-matrix-Commutative-Ring)
+
+  bilinear-map-mul-matrix-Commutative-Ring :
+    bilinear-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-matrix-Commutative-Ring R m n)
+      ( left-module-matrix-Commutative-Ring R n p)
+      ( left-module-matrix-Commutative-Ring R m p)
+  bilinear-map-mul-matrix-Commutative-Ring =
+    ( mul-matrix-Commutative-Ring R m n p ,
+      is-bilinear-map-mul-matrix-Commutative-Ring)
+```
diff --git a/src/linear-algebra/multiplication-matrices-on-rings.lagda.md b/src/linear-algebra/multiplication-matrices-on-rings.lagda.md
new file mode 100644
index 00000000000..4fc0cbc6797
--- /dev/null
+++ b/src/linear-algebra/multiplication-matrices-on-rings.lagda.md
@@ -0,0 +1,242 @@
+# Multiplication of matrices on rings
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.multiplication-matrices-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.matrices-on-rings
+
+open import ring-theory.rings
+open import ring-theory.sums-of-finite-families-of-elements-rings
+open import ring-theory.sums-of-finite-sequences-of-elements-rings
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+In a [ring](ring-theory.rings.md) `R`, the
+{{#concept "product" Disambiguation="of two matrices over a ring" Agda=mul-matrix-Ring}}
+of an `m × n` [matrix](linear-algebra.matrices-on-rings.md) `A` and an `n × p`
+matrix `B` is the `m × p` matrix defined by `(AB)ᵢₖ = ∑ⱼ AᵢⱼBⱼₖ`.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n p : ℕ)
+  where
+
+  mul-matrix-Ring :
+    matrix-Ring R m n → matrix-Ring R n p → matrix-Ring R m p
+  mul-matrix-Ring A B i k =
+    sum-fin-sequence-type-Ring R
+      ( n)
+      ( λ j → mul-Ring R (A i j) (B j k))
+```
+
+## Properties
+
+### Multiplication of matrices is associative
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n p q : ℕ)
+  where
+
+  abstract
+    htpy-associative-mul-matrix-Ring :
+      (A : matrix-Ring R m n)
+      (B : matrix-Ring R n p)
+      (C : matrix-Ring R p q) →
+      binary-htpy
+        ( mul-matrix-Ring R m p q (mul-matrix-Ring R m n p A B) C)
+        ( mul-matrix-Ring R m n q A (mul-matrix-Ring R n p q B C))
+    htpy-associative-mul-matrix-Ring A B C i j =
+      equational-reasoning
+        sum-fin-sequence-type-Ring R
+          ( p)
+          ( λ a →
+            mul-Ring R
+              ( sum-fin-sequence-type-Ring R
+                ( n)
+                ( λ b → mul-Ring R (A i b) (B b a)))
+              ( C a j))
+        ＝
+          sum-fin-sequence-type-Ring R
+            ( p)
+            ( λ a →
+              sum-finite-Ring R
+                ( Fin-Finite-Type n)
+                ( λ b → mul-Ring R (A i b) (mul-Ring R (B b a) (C a j))))
+          by
+            htpy-sum-fin-sequence-type-Ring R
+              ( p)
+              ( λ a →
+                ( right-distributive-mul-sum-fin-sequence-type-Ring R n _ _) ∙
+                ( htpy-sum-fin-sequence-type-Ring R n
+                  ( λ b → associative-mul-Ring R _ _ _)) ∙
+                ( inv (eq-sum-finite-sum-fin-sequence-Ring R n _)))
+        ＝
+          sum-finite-Ring R
+            ( Fin-Finite-Type p)
+            ( λ a →
+              sum-finite-Ring R
+                ( Fin-Finite-Type n)
+                ( λ b → mul-Ring R (A i b) (mul-Ring R (B b a) (C a j))))
+          by inv (eq-sum-finite-sum-fin-sequence-Ring R p _)
+        ＝
+          sum-finite-Ring R
+            ( Fin-Finite-Type n)
+            ( λ b →
+              sum-finite-Ring R
+                ( Fin-Finite-Type p)
+                ( λ a → mul-Ring R (A i b) (mul-Ring R (B b a) (C a j))))
+          by interchange-sum-sum-finite-Ring R _ _ _
+        ＝
+          sum-finite-Ring R
+            ( Fin-Finite-Type n)
+            ( λ b →
+              mul-Ring R
+                ( A i b)
+                ( mul-matrix-Ring R n p q B C b j))
+          by
+            htpy-sum-finite-Ring R _
+              ( λ b →
+                ( eq-sum-finite-sum-fin-sequence-Ring R p _) ∙
+                ( inv
+                  ( left-distributive-mul-sum-fin-sequence-type-Ring R p _ _)))
+        ＝
+          mul-matrix-Ring R m n q
+            ( A)
+            ( mul-matrix-Ring R n p q B C)
+            ( i)
+            ( j)
+          by eq-sum-finite-sum-fin-sequence-Ring R n _
+
+    associative-mul-matrix-Ring :
+      (A : matrix-Ring R m n)
+      (B : matrix-Ring R n p)
+      (C : matrix-Ring R p q) →
+      mul-matrix-Ring R m p q (mul-matrix-Ring R m n p A B) C ＝
+      mul-matrix-Ring R m n q A (mul-matrix-Ring R n p q B C)
+    associative-mul-matrix-Ring A B C =
+      eq-binary-htpy _ _
+        ( htpy-associative-mul-matrix-Ring A B C)
+```
+
+### Left distributivity of matrix multiplication over addition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n p : ℕ)
+  (A : matrix-Ring R m n)
+  (B C : matrix-Ring R n p)
+  where
+
+  abstract
+    htpy-left-distributive-mul-add-matrix-Ring :
+      binary-htpy
+        ( mul-matrix-Ring R m n p A (add-matrix-Ring R n p B C))
+        ( add-matrix-Ring R m p
+          ( mul-matrix-Ring R m n p A B)
+          ( mul-matrix-Ring R m n p A C))
+    htpy-left-distributive-mul-add-matrix-Ring i k =
+      ( htpy-sum-fin-sequence-type-Ring R
+        ( n)
+        ( λ j → left-distributive-mul-add-Ring R _ _ _)) ∙
+      ( inv (interchange-add-sum-fin-sequence-type-Ring R n _ _))
+
+    left-distributive-mul-add-matrix-Ring :
+      mul-matrix-Ring R m n p A (add-matrix-Ring R n p B C) ＝
+      add-matrix-Ring R m p
+        ( mul-matrix-Ring R m n p A B)
+        ( mul-matrix-Ring R m n p A C)
+    left-distributive-mul-add-matrix-Ring =
+      eq-binary-htpy _ _ htpy-left-distributive-mul-add-matrix-Ring
+```
+
+### Right distributivity of matrix multiplication over addition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n p : ℕ)
+  (A B : matrix-Ring R m n)
+  (C : matrix-Ring R n p)
+  where
+
+  abstract
+    htpy-right-distributive-mul-add-matrix-Ring :
+      binary-htpy
+        ( mul-matrix-Ring R m n p (add-matrix-Ring R m n A B) C)
+        ( add-matrix-Ring R m p
+          ( mul-matrix-Ring R m n p A C)
+          ( mul-matrix-Ring R m n p B C))
+    htpy-right-distributive-mul-add-matrix-Ring i k =
+      ( htpy-sum-fin-sequence-type-Ring R
+        ( n)
+        ( λ j → right-distributive-mul-add-Ring R _ _ _)) ∙
+      ( inv (interchange-add-sum-fin-sequence-type-Ring R n _ _))
+
+    right-distributive-mul-add-matrix-Ring :
+      mul-matrix-Ring R m n p (add-matrix-Ring R m n A B) C ＝
+      add-matrix-Ring R m p
+        ( mul-matrix-Ring R m n p A C)
+        ( mul-matrix-Ring R m n p B C)
+    right-distributive-mul-add-matrix-Ring =
+      eq-binary-htpy _ _ htpy-right-distributive-mul-add-matrix-Ring
+```
+
+### `(cA)B = c(AB)`
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (m n p : ℕ)
+  (r : type-Ring R)
+  (A : matrix-Ring R m n)
+  (B : matrix-Ring R n p)
+  where
+
+  abstract
+    htpy-associative-scalar-mul-mul-matrix-Ring :
+      binary-htpy
+        ( mul-matrix-Ring R m n p (scalar-mul-matrix-Ring R m n r A) B)
+        ( scalar-mul-matrix-Ring R m p r (mul-matrix-Ring R m n p A B))
+    htpy-associative-scalar-mul-mul-matrix-Ring i k =
+      ( htpy-sum-fin-sequence-type-Ring R n
+        ( λ j → associative-mul-Ring R r _ _)) ∙
+      ( inv (left-distributive-mul-sum-fin-sequence-type-Ring R n r _))
+
+    associative-scalar-mul-mul-matrix-Ring :
+      mul-matrix-Ring R m n p (scalar-mul-matrix-Ring R m n r A) B ＝
+      scalar-mul-matrix-Ring R m p r (mul-matrix-Ring R m n p A B)
+    associative-scalar-mul-mul-matrix-Ring =
+      eq-binary-htpy _ _ htpy-associative-scalar-mul-mul-matrix-Ring
+```
+
+## See also
+
+- [Multiplication of square matrices on rings](linear-algebra.multiplication-square-matrices-on-rings.md)
diff --git a/src/linear-algebra/multiplication-square-matrices-on-commutative-rings.lagda.md b/src/linear-algebra/multiplication-square-matrices-on-commutative-rings.lagda.md
new file mode 100644
index 00000000000..0685a798a52
--- /dev/null
+++ b/src/linear-algebra/multiplication-square-matrices-on-commutative-rings.lagda.md
@@ -0,0 +1,137 @@
+# Multiplication of square matrices on commutative rings
+
+```agda
+module linear-algebra.multiplication-square-matrices-on-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import group-theory.monoids
+
+open import linear-algebra.bilinear-maps-left-modules-commutative-rings
+open import linear-algebra.identity-matrices-on-commutative-rings
+open import linear-algebra.multiplication-matrices-on-commutative-rings
+open import linear-algebra.multiplication-square-matrices-on-rings
+open import linear-algebra.square-matrices-on-commutative-rings
+```
+
+</details>
+
+## Idea
+
+[Matrix multiplication](linear-algebra.multiplication-matrices-on-commutative-rings.md)
+on [square matrices](linear-algebra.square-matrices-on-commutative-rings.md) on
+a [commutative ring](commutative-algebra.commutative-rings.md) `R` is a
+[bilinear map](linear-algebra.bilinear-maps-left-modules-commutative-rings.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  mul-square-matrix-Commutative-Ring :
+    square-matrix-Commutative-Ring R n →
+    square-matrix-Commutative-Ring R n →
+    square-matrix-Commutative-Ring R n
+  mul-square-matrix-Commutative-Ring =
+    mul-square-matrix-Ring (ring-Commutative-Ring R) n
+```
+
+## Properties
+
+### Associativity of matrix multiplication
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  abstract
+    associative-mul-square-matrix-Commutative-Ring :
+      (A B C : square-matrix-Commutative-Ring R n) →
+      mul-square-matrix-Commutative-Ring R n
+        ( mul-square-matrix-Commutative-Ring R n A B)
+        ( C) ＝
+      mul-square-matrix-Commutative-Ring R n
+        ( A)
+        ( mul-square-matrix-Commutative-Ring R n B C)
+    associative-mul-square-matrix-Commutative-Ring =
+      associative-mul-matrix-Commutative-Ring R n n n n
+```
+
+### Unit laws of square matrix multiplication
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  abstract
+    left-unit-law-mul-square-matrix-Commutative-Ring :
+      (A : square-matrix-Commutative-Ring R n) →
+      mul-square-matrix-Commutative-Ring R n
+        ( id-matrix-Commutative-Ring R n)
+        ( A) ＝
+      A
+    left-unit-law-mul-square-matrix-Commutative-Ring =
+      left-unit-law-mul-square-matrix-Ring (ring-Commutative-Ring R) n
+
+    right-unit-law-mul-square-matrix-Commutative-Ring :
+      (A : square-matrix-Commutative-Ring R n) →
+      mul-square-matrix-Commutative-Ring R n
+        ( A)
+        ( id-matrix-Commutative-Ring R n) ＝
+      A
+    right-unit-law-mul-square-matrix-Commutative-Ring =
+      right-unit-law-mul-square-matrix-Ring (ring-Commutative-Ring R) n
+```
+
+### Multiplication of square matrices in a commutative ring is a bilinear map
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  is-bilinear-map-mul-square-matrix-Commutative-Ring :
+    is-bilinear-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-square-matrix-Commutative-Ring R n)
+      ( left-module-square-matrix-Commutative-Ring R n)
+      ( left-module-square-matrix-Commutative-Ring R n)
+      ( mul-square-matrix-Commutative-Ring R n)
+  is-bilinear-map-mul-square-matrix-Commutative-Ring =
+    is-bilinear-map-mul-matrix-Commutative-Ring R n n n
+
+  bilinear-map-mul-square-matrix-Commutative-Ring :
+    bilinear-map-left-module-Commutative-Ring
+      ( R)
+      ( left-module-square-matrix-Commutative-Ring R n)
+      ( left-module-square-matrix-Commutative-Ring R n)
+      ( left-module-square-matrix-Commutative-Ring R n)
+  bilinear-map-mul-square-matrix-Commutative-Ring =
+    bilinear-map-mul-matrix-Commutative-Ring R n n n
+```
+
+## See also
+
+- [The algebra of square matrices over commutative rings](linear-algebra.algebra-of-square-matrices-on-commutative-rings.md)
diff --git a/src/linear-algebra/multiplication-square-matrices-on-rings.lagda.md b/src/linear-algebra/multiplication-square-matrices-on-rings.lagda.md
new file mode 100644
index 00000000000..f554195e650
--- /dev/null
+++ b/src/linear-algebra/multiplication-square-matrices-on-rings.lagda.md
@@ -0,0 +1,239 @@
+# Multiplication of square matrices on rings
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+module linear-algebra.multiplication-square-matrices-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+open import foundation.coproduct-types
+open import foundation.decidable-propositions
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.singleton-subtypes-discrete-types
+open import foundation.torsorial-type-families
+open import foundation.universe-levels
+
+open import group-theory.monoids
+open import group-theory.semigroups
+
+open import linear-algebra.diagonal-matrices-on-rings
+open import linear-algebra.identity-matrices-on-rings
+open import linear-algebra.multiplication-matrices-on-rings
+open import linear-algebra.square-matrices-on-rings
+
+open import ring-theory.rings
+open import ring-theory.sums-of-finite-families-of-elements-rings
+open import ring-theory.sums-of-finite-sequences-of-elements-rings
+
+open import univalent-combinatorics.decidable-subtypes
+open import univalent-combinatorics.equality-standard-finite-types
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+This file describes properties of
+[multiplication](linear-algebra.multiplication-matrices-on-rings.md) of
+[square matrices](linear-algebra.square-matrices-on-rings.md) on
+[rings](ring-theory.rings.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  mul-square-matrix-Ring :
+    square-matrix-Ring R n → square-matrix-Ring R n → square-matrix-Ring R n
+  mul-square-matrix-Ring = mul-matrix-Ring R n n n
+```
+
+## Properties
+
+### Associativity of square matrix multiplication
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  associative-mul-square-matrix-Ring :
+    (A B C : square-matrix-Ring R n) →
+    mul-square-matrix-Ring R n (mul-square-matrix-Ring R n A B) C ＝
+    mul-square-matrix-Ring R n A (mul-square-matrix-Ring R n B C)
+  associative-mul-square-matrix-Ring =
+    associative-mul-matrix-Ring R n n n n
+```
+
+### The left identity law of square matrix multiplication
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (A : square-matrix-Ring R n)
+  where
+
+  abstract
+    htpy-left-unit-law-mul-square-matrix-Ring :
+      binary-htpy
+        ( mul-square-matrix-Ring R n (id-matrix-Ring R n) A)
+        ( A)
+    htpy-left-unit-law-mul-square-matrix-Ring i j =
+      equational-reasoning
+        sum-fin-sequence-type-Ring R n
+          ( λ k → mul-Ring R (id-matrix-Ring R n i k) (A k j))
+        ＝
+          sum-finite-Ring R
+            ( Fin-Finite-Type n)
+            ( λ k → mul-Ring R (id-matrix-Ring R n i k) (A k j))
+          by inv (eq-sum-finite-sum-fin-sequence-Ring R n _)
+        ＝
+          sum-finite-Ring R
+            ( finite-type-subset-Finite-Type
+              ( Fin-Finite-Type n)
+              ( decidable-standard-singleton-subtype-Discrete-Type
+                ( Fin-Discrete-Type n) i))
+            ( λ (k , i=k) → mul-Ring R (id-matrix-Ring R n i k) (A k j))
+          by
+            vanish-sum-complement-decidable-subset-finite-Ring
+              ( R)
+              ( Fin-Finite-Type n)
+              ( decidable-standard-singleton-subtype-Discrete-Type
+                ( Fin-Discrete-Type n)
+                ( i))
+              ( _)
+              ( λ k i≠k →
+                equational-reasoning
+                  mul-Ring R (id-matrix-Ring R n i k) (A k j)
+                  ＝ mul-Ring R (zero-Ring R) (A k j)
+                    by
+                      ap-mul-Ring R
+                        ( ap
+                          ( rec-coproduct _ _)
+                          ( eq-type-Prop
+                            ( is-decidable-Prop (Id-Prop (Fin-Set n) i k))
+                            { y = inr (i≠k ∘ inv)}))
+                        ( refl)
+                  ＝ zero-Ring R
+                    by left-zero-law-mul-Ring R _)
+        ＝ mul-Ring R (id-matrix-Ring R n i i) (A i j)
+          by sum-finite-is-contr-Ring R _ (is-torsorial-Id' i) (i , refl) _
+        ＝ mul-Ring R (one-Ring R) (A i j)
+          by
+            ap-mul-Ring R
+              ( ap
+                ( rec-coproduct _ _)
+                ( eq-type-Prop
+                  ( is-decidable-Prop (Id-Prop (Fin-Set n) i i))
+                  { y = inl refl}))
+              ( refl)
+        ＝ A i j
+          by left-unit-law-mul-Ring R _
+
+    left-unit-law-mul-square-matrix-Ring :
+      mul-square-matrix-Ring R n (id-matrix-Ring R n) A ＝ A
+    left-unit-law-mul-square-matrix-Ring =
+      eq-binary-htpy _ _ htpy-left-unit-law-mul-square-matrix-Ring
+```
+
+### The right identity law of matrix multiplication
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  (A : square-matrix-Ring R n)
+  where
+
+  abstract
+    htpy-right-unit-law-mul-square-matrix-Ring :
+      binary-htpy
+        ( mul-square-matrix-Ring R n A (id-matrix-Ring R n))
+        ( A)
+    htpy-right-unit-law-mul-square-matrix-Ring i j =
+      equational-reasoning
+        sum-fin-sequence-type-Ring R
+          ( n)
+          ( λ k → mul-Ring R (A i k) (id-matrix-Ring R n k j))
+        ＝
+          sum-finite-Ring R
+            ( Fin-Finite-Type n)
+            ( λ k → mul-Ring R (A i k) (id-matrix-Ring R n k j))
+          by inv (eq-sum-finite-sum-fin-sequence-Ring R n _)
+        ＝
+          sum-finite-Ring R
+            ( finite-type-subset-Finite-Type
+              ( Fin-Finite-Type n)
+              ( decidable-standard-singleton-subtype-Discrete-Type
+                ( Fin-Discrete-Type n)
+                ( j)))
+            ( λ (k , k=j) → mul-Ring R (A i k) (id-matrix-Ring R n k j))
+          by
+            vanish-sum-complement-decidable-subset-finite-Ring
+              ( R)
+              ( Fin-Finite-Type n)
+              ( decidable-standard-singleton-subtype-Discrete-Type
+                ( Fin-Discrete-Type n)
+                ( j))
+              ( _)
+              ( λ k k≠j →
+                equational-reasoning
+                  mul-Ring R (A i k) (id-matrix-Ring R n k j)
+                  ＝ mul-Ring R (A i k) (zero-Ring R)
+                    by
+                      ap-mul-Ring
+                        ( R)
+                        ( refl)
+                        ( ap
+                          ( rec-coproduct _ _)
+                          ( eq-type-Prop
+                            ( is-decidable-Prop (Id-Prop (Fin-Set n) k j))
+                            { y = inr k≠j}))
+                  ＝ zero-Ring R
+                    by right-zero-law-mul-Ring R _)
+        ＝ mul-Ring R (A i j) (id-matrix-Ring R n j j)
+          by sum-finite-is-contr-Ring R _ (is-torsorial-Id' j) (j , refl) _
+        ＝ mul-Ring R (A i j) (one-Ring R)
+          by
+            ap-mul-Ring
+              ( R)
+              ( refl)
+              ( ap
+                ( rec-coproduct _ _)
+                ( eq-type-Prop
+                  ( is-decidable-Prop (Id-Prop (Fin-Set n) j j))
+                  { y = inl refl}))
+        ＝ A i j
+          by right-unit-law-mul-Ring R _
+
+    right-unit-law-mul-square-matrix-Ring :
+      mul-square-matrix-Ring R n A (id-matrix-Ring R n) ＝ A
+    right-unit-law-mul-square-matrix-Ring =
+      eq-binary-htpy _ _ htpy-right-unit-law-mul-square-matrix-Ring
+```
+
+## See also
+
+- [Rings of square matrices on rings](linear-algebra.rings-of-square-matrices-on-rings.md),
+  which shows that square matrices form a ring under multiplication
diff --git a/src/linear-algebra/rings-of-square-matrices-on-rings.lagda.md b/src/linear-algebra/rings-of-square-matrices-on-rings.lagda.md
new file mode 100644
index 00000000000..b9bed48e2f5
--- /dev/null
+++ b/src/linear-algebra/rings-of-square-matrices-on-rings.lagda.md
@@ -0,0 +1,61 @@
+# The rings of square matrices on rings
+
+```agda
+module linear-algebra.rings-of-square-matrices-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import group-theory.monoids
+
+open import linear-algebra.identity-matrices-on-rings
+open import linear-algebra.multiplication-matrices-on-rings
+open import linear-algebra.multiplication-square-matrices-on-rings
+open import linear-algebra.square-matrices-on-rings
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+For any `n : ℕ`, `n × n`
+[square matrices](linear-algebra.square-matrices-on-rings.md) on a
+[ring](ring-theory.rings.md) `R` themselves form a ring under
+[multiplication](linear-algebra.multiplication-square-matrices-on-rings.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  ring-square-matrix-Ring : Ring l
+  ring-square-matrix-Ring =
+    ( ab-square-matrix-Ring R n ,
+      ( mul-square-matrix-Ring R n ,
+        associative-mul-square-matrix-Ring R n) ,
+      ( id-matrix-Ring R n ,
+        left-unit-law-mul-square-matrix-Ring R n ,
+        right-unit-law-mul-square-matrix-Ring R n) ,
+      left-distributive-mul-add-matrix-Ring R n n n ,
+      right-distributive-mul-add-matrix-Ring R n n n)
+
+  monoid-mul-square-matrix-Ring : Monoid l
+  monoid-mul-square-matrix-Ring =
+    multiplicative-monoid-Ring ring-square-matrix-Ring
+```
+
+## See also
+
+- [The algebra of multiplication of square matrices on commutative rings](linear-algebra.algebra-of-square-matrices-on-commutative-rings.md)
diff --git a/src/linear-algebra/scalar-multiplication-matrices.lagda.md b/src/linear-algebra/scalar-multiplication-grids.lagda.md
similarity index 52%
rename from src/linear-algebra/scalar-multiplication-matrices.lagda.md
rename to src/linear-algebra/scalar-multiplication-grids.lagda.md
index e911d6a34fc..fe67ace60f1 100644
--- a/src/linear-algebra/scalar-multiplication-matrices.lagda.md
+++ b/src/linear-algebra/scalar-multiplication-grids.lagda.md
@@ -1,7 +1,7 @@
-# Scalar multiplication on matrices
+# Scalar multiplication on grids
 
 ```agda
-module linear-algebra.scalar-multiplication-matrices where
+module linear-algebra.scalar-multiplication-grids where
 ```
 
 <details><summary>Imports</summary>
@@ -11,15 +11,15 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.universe-levels
 
-open import linear-algebra.matrices
+open import linear-algebra.grids
 open import linear-algebra.scalar-multiplication-tuples
 ```
 
 </details>
 
 ```agda
-scalar-mul-matrix :
+scalar-mul-grid :
   {l1 l2 : Level} {B : UU l1} {A : UU l2} {m n : ℕ} →
-  (B → A → A) → B → matrix A m n → matrix A m n
-scalar-mul-matrix μ = scalar-mul-tuple (scalar-mul-tuple μ)
+  (B → A → A) → B → grid A m n → grid A m n
+scalar-mul-grid μ = scalar-mul-tuple (scalar-mul-tuple μ)
 ```
diff --git a/src/linear-algebra/square-matrices-on-commutative-rings.lagda.md b/src/linear-algebra/square-matrices-on-commutative-rings.lagda.md
new file mode 100644
index 00000000000..e613ca5a08b
--- /dev/null
+++ b/src/linear-algebra/square-matrices-on-commutative-rings.lagda.md
@@ -0,0 +1,53 @@
+# Square matrices on commutative rings
+
+```agda
+module linear-algebra.square-matrices-on-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.left-modules-commutative-rings
+open import linear-algebra.matrices-on-commutative-rings
+open import linear-algebra.square-matrices-on-rings
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "square matrix" Disambiguation="over a commutative ring" WDID=Q2739329 WD="square matrix" Agda=square-matrix-Commutative-Ring}}
+on a [commutative ring](commutative-algebra.commutative-rings.md) `R` of size
+`n` is an `n × n` [matrix](linear-algebra.matrices-on-commutative-rings.md) on
+`R`.
+
+## Definition
+
+```agda
+square-matrix-Commutative-Ring :
+  {l : Level} → Commutative-Ring l → ℕ → UU l
+square-matrix-Commutative-Ring R = square-matrix-Ring (ring-Commutative-Ring R)
+```
+
+## Properties
+
+### Square matrices on a commutative ring form a left module
+
+```agda
+module _
+  {l : Level}
+  (R : Commutative-Ring l)
+  (n : ℕ)
+  where
+
+  left-module-square-matrix-Commutative-Ring : left-module-Commutative-Ring l R
+  left-module-square-matrix-Commutative-Ring =
+    left-module-matrix-Commutative-Ring R n n
+```
diff --git a/src/linear-algebra/square-matrices-on-rings.lagda.md b/src/linear-algebra/square-matrices-on-rings.lagda.md
new file mode 100644
index 00000000000..268f9aa459a
--- /dev/null
+++ b/src/linear-algebra/square-matrices-on-rings.lagda.md
@@ -0,0 +1,63 @@
+# Square matrices on rings
+
+```agda
+module linear-algebra.square-matrices-on-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.matrices-on-rings
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "square matrix" Disambiguation="over a ring" WDID=Q2739329 WD="square matrix" Agda=square-matrix-Ring}}
+on a [ring](ring-theory.rings.md) `R` is a
+[matrix](linear-algebra.matrices-on-rings.md) over `R` that is `n × n` for some
+`n`.
+
+## Definition
+
+```agda
+square-matrix-Ring : {l : Level} → Ring l → ℕ → UU l
+square-matrix-Ring R n = matrix-Ring R n n
+```
+
+## Properties
+
+### Square matrices in a ring form a set
+
+```agda
+set-square-matrix-Ring : {l : Level} → Ring l → ℕ → Set l
+set-square-matrix-Ring R n = set-matrix-Ring R n n
+```
+
+### Square matrices on a ring form a left module
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  left-module-square-matrix-Ring : left-module-Ring l R
+  left-module-square-matrix-Ring = left-module-matrix-Ring R n n
+
+  ab-square-matrix-Ring : Ab l
+  ab-square-matrix-Ring = ab-matrix-Ring R n n
+```
diff --git a/src/linear-algebra/square-matrices.lagda.md b/src/linear-algebra/square-matrices.lagda.md
new file mode 100644
index 00000000000..9561071e8c7
--- /dev/null
+++ b/src/linear-algebra/square-matrices.lagda.md
@@ -0,0 +1,30 @@
+# Square matrices
+
+```agda
+module linear-algebra.square-matrices where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.matrices
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "square matrix" WD="square matrix" WDID=Q2739329 Agda=square-matrix}}
+is a [matrix](linear-algebra.matrices.md) that is `n × n` for some `n`.
+
+## Definition
+
+```agda
+square-matrix : {l : Level} → UU l → ℕ → UU l
+square-matrix A n = matrix A n n
+```
diff --git a/src/linear-algebra/sums-of-finite-sequences-of-elements-left-modules-commutative-rings.lagda.md b/src/linear-algebra/sums-of-finite-sequences-of-elements-left-modules-commutative-rings.lagda.md
new file mode 100644
index 00000000000..2cd4e581f6f
--- /dev/null
+++ b/src/linear-algebra/sums-of-finite-sequences-of-elements-left-modules-commutative-rings.lagda.md
@@ -0,0 +1,49 @@
+# Sums of finite sequences of elements in left modules over commutative rings
+
+```agda
+module linear-algebra.sums-of-finite-sequences-of-elements-left-modules-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
+
+open import linear-algebra.left-modules-commutative-rings
+
+open import lists.finite-sequences
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "sum" Disambiguation="of elements of left modules over commutative rings" Agda=sum-fin-sequence-type-left-module-Commutative-Ring}}
+operation on [left modules](linear-algebra.left-modules-commutative-rings.md)
+over [commutative rings](commutative-algebra.commutative-rings.md) generalizes
+its binary addition operation to any
+[finite sequence](lists.finite-sequences.md) of elements of the module.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Commutative-Ring l1)
+  (M : left-module-Commutative-Ring l2 R)
+  where
+
+  sum-fin-sequence-type-left-module-Commutative-Ring :
+    (n : ℕ) →
+    fin-sequence (type-left-module-Commutative-Ring R M) n →
+    type-left-module-Commutative-Ring R M
+  sum-fin-sequence-type-left-module-Commutative-Ring =
+    sum-fin-sequence-type-Ab (ab-left-module-Commutative-Ring R M)
+```
diff --git a/src/linear-algebra/sums-of-finite-sequences-of-elements-left-modules-rings.lagda.md b/src/linear-algebra/sums-of-finite-sequences-of-elements-left-modules-rings.lagda.md
new file mode 100644
index 00000000000..b965f3409a7
--- /dev/null
+++ b/src/linear-algebra/sums-of-finite-sequences-of-elements-left-modules-rings.lagda.md
@@ -0,0 +1,47 @@
+# Sums of finite sequences of elements in left modules over rings
+
+```agda
+module linear-algebra.sums-of-finite-sequences-of-elements-left-modules-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
+
+open import linear-algebra.left-modules-rings
+
+open import lists.finite-sequences
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "sum" Disambiguation="of elements of left modules over rings" Agda=sum-fin-sequence-type-left-module-Ring}}
+operation on [left modules](linear-algebra.left-modules-rings.md) over
+[rings](ring-theory.rings.md) generalizes its binary addition operation to any
+[finite sequence](lists.finite-sequences.md) of elements of the module.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  sum-fin-sequence-type-left-module-Ring :
+    (n : ℕ) →
+    fin-sequence (type-left-module-Ring R M) n → type-left-module-Ring R M
+  sum-fin-sequence-type-left-module-Ring =
+    sum-fin-sequence-type-Ab (ab-left-module-Ring R M)
+```
diff --git a/src/linear-algebra/symmetric-matrices.lagda.md b/src/linear-algebra/symmetric-matrices.lagda.md
new file mode 100644
index 00000000000..ff453921501
--- /dev/null
+++ b/src/linear-algebra/symmetric-matrices.lagda.md
@@ -0,0 +1,36 @@
+# Symmetric matrices
+
+```agda
+module linear-algebra.symmetric-matrices where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-homotopies
+open import foundation.sets
+open import foundation.universe-levels
+
+open import linear-algebra.square-matrices
+open import linear-algebra.transposition-matrices
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "symmetric matrix" WDID=Q339011 WD="symmetric matrix" Agda=is-symmetric-square-matrix}}
+is a [square matrix](linear-algebra.square-matrices.md) `M` with `Mᵢⱼ = Mⱼᵢ` for
+all `i` and `j`.
+
+## Definition
+
+```agda
+is-symmetric-square-matrix :
+  {l : Level} {A : UU l} (n : ℕ) → square-matrix A n → UU l
+is-symmetric-square-matrix n M =
+  binary-htpy (transpose-square-matrix n M) M
+```
diff --git a/src/linear-algebra/transposition-grids.lagda.md b/src/linear-algebra/transposition-grids.lagda.md
new file mode 100644
index 00000000000..de65adc2e3e
--- /dev/null
+++ b/src/linear-algebra/transposition-grids.lagda.md
@@ -0,0 +1,71 @@
+# Transposition of grids
+
+```agda
+module linear-algebra.transposition-grids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.grids
+
+open import lists.functoriality-tuples
+open import lists.tuples
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "transposition of a grid" WD="grid transposition" WDID=Q77961711 Agda=transpose-grid}}
+is the operation on [grids](linear-algebra.grids.md) that turns rows into
+columns and columns into rows.
+
+## Definition
+
+```agda
+transpose-grid :
+  {l : Level} → {A : UU l} → {m n : ℕ} → grid A m n → grid A n m
+transpose-grid {n = zero-ℕ} x = empty-tuple
+transpose-grid {n = succ-ℕ n} x =
+  map-tuple head-tuple x ∷ transpose-grid (map-tuple tail-tuple x)
+```
+
+## Properties
+
+```agda
+is-involution-transpose-grid :
+  {l : Level} → {A : UU l} → {m n : ℕ} →
+  (x : grid A m n) → x ＝ transpose-grid (transpose-grid x)
+is-involution-transpose-grid {m = zero-ℕ} empty-tuple = refl
+is-involution-transpose-grid {m = succ-ℕ m} (r ∷ rs) =
+  ( ap (_∷_ r) (is-involution-transpose-grid rs)) ∙
+  ( ap-binary _∷_
+    ( lemma-first-row r rs) (ap transpose-grid (lemma-rest r rs)))
+  where
+  lemma-first-row :
+    {l : Level} → {A : UU l} → {m n : ℕ} → (x : tuple A n) →
+    (xs : grid A m n) →
+    x ＝ map-tuple head-tuple (transpose-grid (x ∷ xs))
+  lemma-first-row {n = zero-ℕ} empty-tuple _ = refl
+  lemma-first-row {n = succ-ℕ m} (k ∷ ks) xs =
+    ap (_∷_ k) (lemma-first-row ks (map-tuple tail-tuple xs))
+
+  lemma-rest :
+    {l : Level} → {A : UU l} → {m n : ℕ} → (x : tuple A n) →
+    (xs : grid A m n) →
+    transpose-grid xs ＝ map-tuple tail-tuple (transpose-grid (x ∷ xs))
+  lemma-rest {n = zero-ℕ} empty-tuple xs = refl
+  lemma-rest {n = succ-ℕ n} (k ∷ ks) xs =
+    ap
+      ( _∷_ (map-tuple head-tuple xs))
+      ( lemma-rest (tail-tuple (k ∷ ks)) (map-tuple tail-tuple xs))
+```
diff --git a/src/linear-algebra/transposition-matrices.lagda.md b/src/linear-algebra/transposition-matrices.lagda.md
index 72d36918e13..c5c9a36419e 100644
--- a/src/linear-algebra/transposition-matrices.lagda.md
+++ b/src/linear-algebra/transposition-matrices.lagda.md
@@ -9,15 +9,10 @@ module linear-algebra.transposition-matrices where
 ```agda
 open import elementary-number-theory.natural-numbers
 
-open import foundation.action-on-identifications-binary-functions
-open import foundation.action-on-identifications-functions
-open import foundation.identity-types
 open import foundation.universe-levels
 
 open import linear-algebra.matrices
-
-open import lists.functoriality-tuples
-open import lists.tuples
+open import linear-algebra.square-matrices
 ```
 
 </details>
@@ -25,47 +20,17 @@ open import lists.tuples
 ## Idea
 
 The
-{{#concept "transposition of a matrix" WD="matrix transposition" WDID=Q77961711 Agda=transpose-matrix}}
-is the operation on [matrices](linear-algebra.matrices.md) that turns rows into
-columns and columns into rows.
+{{#concept "transpose" WDID=Q77961711 WD="matrix transposition" Agda=transpose-matrix}}
+of a [matrix](linear-algebra.matrices.md) `M` is the matrix `Mᵀᵢⱼ ≔ Mⱼᵢ`.
 
 ## Definition
 
 ```agda
 transpose-matrix :
-  {l : Level} → {A : UU l} → {m n : ℕ} → matrix A m n → matrix A n m
-transpose-matrix {n = zero-ℕ} x = empty-tuple
-transpose-matrix {n = succ-ℕ n} x =
-  map-tuple head-tuple x ∷ transpose-matrix (map-tuple tail-tuple x)
-```
-
-## Properties
-
-```agda
-is-involution-transpose-matrix :
-  {l : Level} → {A : UU l} → {m n : ℕ} →
-  (x : matrix A m n) → x ＝ transpose-matrix (transpose-matrix x)
-is-involution-transpose-matrix {m = zero-ℕ} empty-tuple = refl
-is-involution-transpose-matrix {m = succ-ℕ m} (r ∷ rs) =
-  ( ap (_∷_ r) (is-involution-transpose-matrix rs)) ∙
-  ( ap-binary _∷_
-    ( lemma-first-row r rs) (ap transpose-matrix (lemma-rest r rs)))
-  where
-  lemma-first-row :
-    {l : Level} → {A : UU l} → {m n : ℕ} → (x : tuple A n) →
-    (xs : matrix A m n) →
-    x ＝ map-tuple head-tuple (transpose-matrix (x ∷ xs))
-  lemma-first-row {n = zero-ℕ} empty-tuple _ = refl
-  lemma-first-row {n = succ-ℕ m} (k ∷ ks) xs =
-    ap (_∷_ k) (lemma-first-row ks (map-tuple tail-tuple xs))
+  {l : Level} {A : UU l} (m n : ℕ) → matrix A m n → matrix A n m
+transpose-matrix m n M i j = M j i
 
-  lemma-rest :
-    {l : Level} → {A : UU l} → {m n : ℕ} → (x : tuple A n) →
-    (xs : matrix A m n) →
-    transpose-matrix xs ＝ map-tuple tail-tuple (transpose-matrix (x ∷ xs))
-  lemma-rest {n = zero-ℕ} empty-tuple xs = refl
-  lemma-rest {n = succ-ℕ n} (k ∷ ks) xs =
-    ap
-      ( _∷_ (map-tuple head-tuple xs))
-      ( lemma-rest (tail-tuple (k ∷ ks)) (map-tuple tail-tuple xs))
+transpose-square-matrix :
+  {l : Level} {A : UU l} (n : ℕ) → square-matrix A n → square-matrix A n
+transpose-square-matrix n = transpose-matrix n n
 ```
diff --git a/src/ring-theory/sums-of-finite-families-of-elements-rings.lagda.md b/src/ring-theory/sums-of-finite-families-of-elements-rings.lagda.md
index 6358f9fcaa5..6505de4c004 100644
--- a/src/ring-theory/sums-of-finite-families-of-elements-rings.lagda.md
+++ b/src/ring-theory/sums-of-finite-families-of-elements-rings.lagda.md
@@ -7,23 +7,35 @@ module ring-theory.sums-of-finite-families-of-elements-rings where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.negation
+open import foundation.type-arithmetic-cartesian-product-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import linear-algebra.finite-sequences-in-rings
+
 open import ring-theory.rings
 open import ring-theory.sums-of-finite-families-of-elements-semirings
 open import ring-theory.sums-of-finite-sequences-of-elements-rings
 
+open import univalent-combinatorics.complements-decidable-subtypes
 open import univalent-combinatorics.coproduct-types
 open import univalent-combinatorics.counting
+open import univalent-combinatorics.decidable-subtypes
 open import univalent-combinatorics.dependent-pair-types
 open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -190,3 +202,108 @@ eq-sum-finite-sum-count-Ring :
 eq-sum-finite-sum-count-Ring R =
   eq-sum-finite-sum-count-Semiring (semiring-Ring R)
 ```
+
+### The sum of a finite sequence is the sum over the type of indices of that sequence
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  (n : ℕ)
+  where
+
+  abstract
+    eq-sum-finite-sum-fin-sequence-Ring :
+      (u : fin-sequence-type-Ring R n) →
+      sum-finite-Ring R (Fin-Finite-Type n) u ＝ sum-fin-sequence-type-Ring R n u
+    eq-sum-finite-sum-fin-sequence-Ring =
+      eq-sum-finite-sum-count-Ring R (Fin-Finite-Type n) (count-Fin n)
+```
+
+### Interchanging nested sums
+
+```agda
+module _
+  {l1 l2 l3 : Level} (R : Ring l1)
+  (A : Finite-Type l2) (B : Finite-Type l3)
+  where
+
+  abstract
+    interchange-sum-sum-finite-Ring :
+      (u : type-Finite-Type A → type-Finite-Type B → type-Ring R) →
+      sum-finite-Ring R A (λ a → sum-finite-Ring R B (λ b → u a b)) ＝
+      sum-finite-Ring R B (λ b → sum-finite-Ring R A (λ a → u a b))
+    interchange-sum-sum-finite-Ring u =
+      equational-reasoning
+        sum-finite-Ring R A (λ a → sum-finite-Ring R B (u a))
+        ＝ sum-finite-Ring R (Σ-Finite-Type A (λ _ → B)) (ind-Σ u)
+          by inv (sum-Σ-finite-Ring R A (λ _ → B) u)
+        ＝ sum-finite-Ring R (Σ-Finite-Type B (λ _ → A)) (λ (b , a) → u a b)
+          by
+            sum-equiv-finite-Ring R
+              ( Σ-Finite-Type A (λ _ → B))
+              ( Σ-Finite-Type B (λ _ → A))
+              ( commutative-product)
+              ( ind-Σ u)
+        ＝ sum-finite-Ring R B (λ b → sum-finite-Ring R A (λ a → u a b))
+          by sum-Σ-finite-Ring R B (λ _ → A) (λ b a → u a b)
+```
+
+### Sums that vanish on a decidable subtype
+
+```agda
+module _
+  {l1 l2 l3 : Level} (R : Ring l1) (A : Finite-Type l2)
+  (P : subset-Finite-Type l3 A)
+  where
+
+  abstract
+    vanish-sum-decidable-subset-finite-Ring :
+      (f : type-Finite-Type A → type-Ring R) →
+      ( (a : type-Finite-Type A) → is-in-decidable-subtype P a →
+        is-zero-Ring R (f a)) →
+      sum-finite-Ring R A f ＝
+      sum-finite-Ring R
+        ( finite-type-complement-subset-Finite-Type A P)
+        ( f ∘ inclusion-complement-subset-Finite-Type A P)
+    vanish-sum-decidable-subset-finite-Ring =
+      vanish-sum-decidable-subset-finite-Ab
+        ( ab-Ring R)
+        ( A)
+        ( P)
+
+    vanish-sum-complement-decidable-subset-finite-Ring :
+      (f : type-Finite-Type A → type-Ring R) →
+      ( (a : type-Finite-Type A) → ¬ (is-in-decidable-subtype P a) →
+        is-zero-Ring R (f a)) →
+      sum-finite-Ring R A f ＝
+      sum-finite-Ring R
+        ( finite-type-subset-Finite-Type A P)
+        ( f ∘ inclusion-subset-Finite-Type A P)
+    vanish-sum-complement-decidable-subset-finite-Ring =
+      vanish-sum-complement-decidable-subset-finite-Ab
+        ( ab-Ring R)
+        ( A)
+        ( P)
+```
+
+### Sums over contractible types
+
+```agda
+module _
+  {l1 l2 : Level} (R : Ring l1) (I : Finite-Type l2)
+  (is-contr-I : is-contr (type-Finite-Type I))
+  (i : type-Finite-Type I)
+  where
+
+  abstract
+    sum-finite-is-contr-Ring :
+      (f : type-Finite-Type I → type-Ring R) →
+      sum-finite-Ring R I f ＝ f i
+    sum-finite-is-contr-Ring =
+      sum-finite-is-contr-Ab
+        ( ab-Ring R)
+        ( I)
+        ( is-contr-I)
+        ( i)
+```