diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index ba50e0c42c..a97e32831d 100644
--- a/src/linear-algebra.lagda.md
+++ b/src/linear-algebra.lagda.md
@@ -24,8 +24,10 @@ open import linear-algebra.finite-sequences-in-semirings public
 open import linear-algebra.functoriality-matrices public
 open import linear-algebra.left-modules-commutative-rings public
 open import linear-algebra.left-modules-rings public
+open import linear-algebra.left-modules-with-ordered-bases-rings public
 open import linear-algebra.left-submodules-rings public
 open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings public
+open import linear-algebra.linear-independence-left-modules-rings public
 open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.linear-spans-left-modules-rings public
 open import linear-algebra.matrices public
diff --git a/src/linear-algebra/left-modules-rings.lagda.md b/src/linear-algebra/left-modules-rings.lagda.md
index 6bc9d5ff41..b9ba8fdbd0 100644
--- a/src/linear-algebra/left-modules-rings.lagda.md
+++ b/src/linear-algebra/left-modules-rings.lagda.md
@@ -7,6 +7,7 @@ module linear-algebra.left-modules-rings where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.ring-of-integers
 
 open import foundation.action-on-identifications-functions
diff --git a/src/linear-algebra/left-modules-with-ordered-bases-rings.lagda.md b/src/linear-algebra/left-modules-with-ordered-bases-rings.lagda.md
new file mode 100644
index 0000000000..a8bf14db4f
--- /dev/null
+++ b/src/linear-algebra/left-modules-with-ordered-bases-rings.lagda.md
@@ -0,0 +1,51 @@
+# Left modules over rings with ordered basis
+
+```agda
+module linear-algebra.left-modules-with-ordered-bases-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 foundation-core.cartesian-product-types
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.linear-independence-left-modules-rings
+open import linear-algebra.linear-spans-left-modules-rings
+open import linear-algebra.subsets-left-modules-rings
+
+open import lists.tuples
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "left module over a ring with an ordered basis" Agda=left-module-with-ordered-basis-Ring}}
+is a [left module](linear-algebra.left-modules-rings.md) `M` over a
+[ring](ring-theory.rings.md) `R` with a linearly independent tuple whose linear
+span is the whole of `M`.
+
+## Definitions
+
+### Left modules over rings with ordered bases
+
+```agda
+left-module-with-ordered-basis-Ring :
+  {l1 : Level} (n : ℕ) (l : Level) (R : Ring l1) → UU (l1 ⊔ lsuc l)
+left-module-with-ordered-basis-Ring {l1} n l R =
+  Σ
+    ( Σ ( left-module-Ring l R)
+        ( λ M → linearly-independent-tuple-left-module-Ring n R M))
+    ( λ (M , b) → is-linear-span-subset-left-module-Ring R M
+      ( whole-subset-left-module-Ring R M)
+      ( subset-tuple (tuple-linearly-independent-tuple R M b)))
+```
diff --git a/src/linear-algebra/linear-combinations-tuples-of-vectors-left-modules-rings.lagda.md b/src/linear-algebra/linear-combinations-tuples-of-vectors-left-modules-rings.lagda.md
index acaedba8a7..e9bfa06f4e 100644
--- a/src/linear-algebra/linear-combinations-tuples-of-vectors-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-combinations-tuples-of-vectors-left-modules-rings.lagda.md
@@ -12,6 +12,11 @@ open import elementary-number-theory.natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.identity-types
 open import foundation.universe-levels
+open import foundation.coproduct-types
+
+open import foundation-core.identity-types
+
+open import univalent-combinatorics.standard-finite-types
 
 open import linear-algebra.left-modules-rings
 
@@ -291,3 +296,143 @@ module _
             ( vectors-b))
         by refl
 ```
+
+###
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  zero-trivial-tuple-linear-combination-tuple-left-module-Ring :
+    (n : ℕ) →
+    (vectors : tuple (type-left-module-Ring R M) n) →
+    linear-combination-tuple-left-module-Ring R M
+      ( trivial-tuple-Ring R n)
+      ( vectors) ＝
+    zero-left-module-Ring R M
+  zero-trivial-tuple-linear-combination-tuple-left-module-Ring n empty-tuple =
+    refl
+  zero-trivial-tuple-linear-combination-tuple-left-module-Ring
+    (succ-ℕ n) (x ∷ vectors) =
+    equational-reasoning
+    linear-combination-tuple-left-module-Ring R M
+      ( zero-Ring R ∷ trivial-tuple-Ring R n)
+      ( x ∷ vectors)
+    ＝ add-left-module-Ring R M
+      ( linear-combination-tuple-left-module-Ring R M
+        ( trivial-tuple-Ring R n)
+        ( vectors))
+      ( mul-left-module-Ring R M (zero-Ring R) x)
+      by refl
+    ＝ add-left-module-Ring R M
+      ( linear-combination-tuple-left-module-Ring R M
+        ( trivial-tuple-Ring R n)
+        ( vectors))
+      ( zero-left-module-Ring R M)
+      by
+        ap
+          ( λ y → add-left-module-Ring R M
+            ( linear-combination-tuple-left-module-Ring R M
+              ( trivial-tuple-Ring R n)
+              ( vectors))
+            ( y))
+          (left-zero-law-mul-left-module-Ring R M x)
+    ＝ add-left-module-Ring R M
+      ( zero-left-module-Ring R M)
+      ( zero-left-module-Ring R M)
+      by
+        ap
+          ( λ y → add-left-module-Ring R M y (zero-left-module-Ring R M))
+          ( zero-trivial-tuple-linear-combination-tuple-left-module-Ring n
+            ( vectors))
+    ＝ zero-left-module-Ring R M
+      by left-unit-law-add-left-module-Ring R M (zero-left-module-Ring R M)
+```
+
+###
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  component-with-value-tuple-trivial-tuple-linear-combination-tuple-left-module-Ring :
+    (n : ℕ) →
+    (r : type-Ring R)
+    (vectors : tuple (type-left-module-Ring R M) n) →
+    (i : Fin n) →
+    linear-combination-tuple-left-module-Ring R M
+      ( with-value-tuple i r (trivial-tuple-Ring R n))
+      ( vectors) ＝
+    mul-left-module-Ring R M r (component-tuple n vectors i)
+  component-with-value-tuple-trivial-tuple-linear-combination-tuple-left-module-Ring
+    (succ-ℕ n) r (x ∷ vectors) (inr _) =
+    equational-reasoning
+    linear-combination-tuple-left-module-Ring R M
+      ( with-value-tuple (inr _) r (trivial-tuple-Ring R (succ-ℕ n)))
+      ( x ∷ vectors)
+    ＝ linear-combination-tuple-left-module-Ring R M
+      ( r ∷ (trivial-tuple-Ring R n))
+      ( x ∷ vectors)
+      by refl
+    ＝ add-left-module-Ring R M
+      ( linear-combination-tuple-left-module-Ring R M
+        ( trivial-tuple-Ring R n)
+        ( vectors))
+      ( mul-left-module-Ring R M r x)
+      by refl
+    ＝ add-left-module-Ring R M
+      ( zero-left-module-Ring R M)
+      ( mul-left-module-Ring R M r x)
+      by
+        ap
+          ( λ y → add-left-module-Ring R M y (mul-left-module-Ring R M r x))
+          (zero-trivial-tuple-linear-combination-tuple-left-module-Ring R M n vectors)
+    ＝ mul-left-module-Ring R M r x
+      by left-unit-law-add-left-module-Ring R M (mul-left-module-Ring R M r x)
+    ＝ mul-left-module-Ring R M r (component-tuple (succ-ℕ n) (x ∷ vectors) (inr _))
+      by ap (λ y → mul-left-module-Ring R M r y) refl
+  component-with-value-tuple-trivial-tuple-linear-combination-tuple-left-module-Ring
+    (succ-ℕ n) r (x ∷ vectors) (inl i) =
+    equational-reasoning
+    linear-combination-tuple-left-module-Ring R M
+      ( with-value-tuple (inl i) r (trivial-tuple-Ring R (succ-ℕ n)))
+      ( x ∷ vectors)
+    ＝ linear-combination-tuple-left-module-Ring R M
+      ( zero-Ring R ∷ (with-value-tuple i r (trivial-tuple-Ring R n)))
+      ( x ∷ vectors)
+      by refl
+    ＝ add-left-module-Ring R M
+      ( linear-combination-tuple-left-module-Ring R M
+        ( with-value-tuple i r (trivial-tuple-Ring R n))
+        ( vectors))
+      ( mul-left-module-Ring R M (zero-Ring R) x)
+      by refl
+    ＝ add-left-module-Ring R M
+      ( linear-combination-tuple-left-module-Ring R M
+        ( with-value-tuple i r (trivial-tuple-Ring R n))
+        ( vectors))
+      ( zero-left-module-Ring R M)
+      by
+        ap
+          ( λ y → add-left-module-Ring R M
+            ( linear-combination-tuple-left-module-Ring R M
+              ( with-value-tuple i r (trivial-tuple-Ring R n))
+              ( vectors))
+            ( y))
+          ( left-zero-law-mul-left-module-Ring R M x)
+    ＝ linear-combination-tuple-left-module-Ring R M
+        ( with-value-tuple i r (trivial-tuple-Ring R n))
+        ( vectors)
+      by right-unit-law-add-left-module-Ring R M
+        ( linear-combination-tuple-left-module-Ring R M
+          ( with-value-tuple i r (trivial-tuple-Ring R n))
+          ( vectors))
+    ＝ mul-left-module-Ring R M r (component-tuple (succ-ℕ n) (x ∷ vectors) (inl i))
+      by component-with-value-tuple-trivial-tuple-linear-combination-tuple-left-module-Ring n r vectors i
+```
diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
new file mode 100644
index 0000000000..c4b18dbe9c
--- /dev/null
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -0,0 +1,278 @@
+# Linear independence
+
+```agda
+module linear-algebra.linear-independence-left-modules-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.distance-natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+open import elementary-number-theory.addition-natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.negation
+open import foundation.negated-equality
+open import foundation.universe-levels
+open import foundation.action-on-identifications-functions
+
+open import foundation-core.sets
+open import foundation-core.empty-types
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.subsets-left-modules-rings
+open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings
+
+open import lists.tuples
+open import lists.functoriality-tuples
+open import lists.concatenation-tuples
+
+open import ring-theory.rings
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+Let `M` be a [left module](linear-algebra.left-modules-rings.md) over a
+[ring](ring-theory.rings.md) `R`.
+
+A tuple `x_1, ..., x_n` of elements of `M` is a
+{{#concept "linearly independent tuple" Agda=is-linearly-independent-tuple-left-module-prop-Ring Agda=linearly-independent-tuple-left-module-Ring}},
+if `r_1 * x_1 + ... + r_n * x_n = 0` implies `r_1 = ... = r_n = 0`.
+
+A subset `S` of `M` is a
+{{#concept "linearly independent subset" Agda=is-linearly-independent-subset-left-module-prop-Ring Agda=linearly-independent-subset-left-module-Ring}}
+if any tuple `x_1, ..., x_n` of elements of `S` is linearly independent.
+
+## Definitions
+
+### The condition of a tuple being linearly independent
+
+```agda
+module _
+  {l1 l2 : Level}
+  {n : ℕ}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (vectors : tuple (type-left-module-Ring R M) n)
+  where
+
+  is-linearly-independent-tuple-left-module-prop-Ring : Prop (l1 ⊔ l2)
+  is-linearly-independent-tuple-left-module-prop-Ring =
+    Π-Prop
+      ( tuple (type-Ring R) n)
+      λ scalars →
+        hom-Prop
+          ( Id-Prop
+            ( set-left-module-Ring R M)
+            ( linear-combination-tuple-left-module-Ring R M scalars vectors)
+            ( zero-left-module-Ring R M))
+          ( Id-Prop
+            ( tuple-Set (set-Ring R) n)
+            ( scalars)
+            ( trivial-tuple-Ring R n))
+
+  is-linearly-independent-tuple-left-module-Ring : UU (l1 ⊔ l2)
+  is-linearly-independent-tuple-left-module-Ring =
+    type-Prop is-linearly-independent-tuple-left-module-prop-Ring
+```
+
+### Linearly independent tuple in a left-module over a ring
+
+```agda
+linearly-independent-tuple-left-module-Ring :
+  {l1 l2 : Level}
+  (R : Ring l1) (M : left-module-Ring l2 R) (n : ℕ) → UU (l1 ⊔ l2)
+linearly-independent-tuple-left-module-Ring R M n =
+  Σ ( tuple (type-left-module-Ring R M) n)
+    ( λ v → is-linearly-independent-tuple-left-module-Ring R M v)
+
+module _
+  {l1 l2 : Level}
+  {n : ℕ}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (vectors : linearly-independent-tuple-left-module-Ring R M n)
+  where
+
+  tuple-linearly-independent-tuple : tuple (type-left-module-Ring R M) n
+  tuple-linearly-independent-tuple = pr1 vectors
+```
+
+### The condition of a subset being linearly independent
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (S : subset-left-module-Ring l3 R M)
+  where
+
+  is-linearly-independent-subset-left-module-prop-Ring : Prop (l1 ⊔ l2 ⊔ l3)
+  is-linearly-independent-subset-left-module-prop-Ring =
+    Π-Prop
+      ( ℕ)
+      ( λ n →
+        Π-Prop
+          ( tuple (type-subset-left-module-Ring R M S) n)
+          ( λ vectors → is-linearly-independent-tuple-left-module-prop-Ring R M
+            ( map-tuple (inclusion-subset-left-module-Ring R M S) vectors)))
+
+  is-linearly-independent-subset-left-module-Ring : UU (l1 ⊔ l2 ⊔ l3)
+  is-linearly-independent-subset-left-module-Ring =
+    type-Prop is-linearly-independent-subset-left-module-prop-Ring
+```
+
+### Linearly independent subset of a left module over a ring
+
+```agda
+linearly-independent-subset-left-module-Ring :
+  {l1 l2 : Level}
+  (l3 : Level) (R : Ring l1) (M : left-module-Ring l2 R) →
+  UU (l1 ⊔ l2 ⊔ lsuc l3)
+linearly-independent-subset-left-module-Ring l3 R M =
+  Σ ( subset-left-module-Ring l3 R M)
+    ( λ S → is-linearly-independent-subset-left-module-Ring R M S)
+
+module _
+  {l1 l2 l3 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (S : linearly-independent-subset-left-module-Ring l3 R M)
+  where
+
+  subset-linearly-independent-tuple : subset-left-module-Ring l3 R M
+  subset-linearly-independent-tuple = pr1 S
+```
+
+## Properties
+
+### A tuple with a repeating element is linearly dependent
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring :
+    (n : ℕ) → (i j : Fin n) → tuple (type-Ring R) n
+  non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring n i j =
+    ( with-value-tuple i
+      ( one-Ring R)
+      ( with-value-tuple j (neg-one-Ring R) (trivial-tuple-Ring R n)))
+
+  gives-zero-linearly-dependent-repeated-element-tuple :
+    (n : ℕ) →
+    (vectors : tuple (type-left-module-Ring R M) n) →
+    (i j : Fin n) →
+    (i ≠ j) →
+    (component-tuple n vectors i ＝ component-tuple n vectors j) →
+    linear-combination-tuple-left-module-Ring R M
+      ( non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring n i j)
+      ( vectors) ＝
+    zero-left-module-Ring R M
+  gives-zero-linearly-dependent-repeated-element-tuple n vectors i j i≠j identity = {! !}
+
+  linearly-dependent-repeated-element-tuple-left-module-Ring :
+    (zero-is-not-one-Ring R) →
+    (n : ℕ) →
+    (vectors : tuple (type-left-module-Ring R M) n) →
+    (i j : Fin n) →
+    (i ≠ j) →
+    (component-tuple n vectors i ＝ component-tuple n vectors j) →
+    ¬ is-linearly-independent-tuple-left-module-Ring R M vectors
+  linearly-dependent-repeated-element-tuple-left-module-Ring
+    zero-is-not-one n vectors i j i≠j identity implies-trivial-tuple =
+    zero-is-not-one
+      ( equational-reasoning
+        zero-Ring R
+        ＝ component-tuple n (trivial-tuple-Ring R n) i
+          by zero-component-trivial-tuple n i
+        ＝ component-tuple n
+            ( non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring
+              ( n)
+              ( i)
+              ( j))
+            ( i )
+          by
+            elements-equal-tuple
+              ( n)
+              ( i)
+              ( trivial-tuple-Ring R n)
+              ( non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring
+                ( n)
+                ( i)
+                ( j))
+              ( inv
+                ( implies-trivial-tuple
+                  ( non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring
+                    ( n)
+                    ( i)
+                    ( j))
+                  ( gives-zero-linearly-dependent-repeated-element-tuple
+                    ( n)
+                    ( vectors)
+                    ( i)
+                    ( j)
+                    ( i≠j)
+                    ( identity))))
+        ＝ component-tuple n
+          ( with-value-tuple i (one-Ring R)
+            ( with-value-tuple j (neg-one-Ring R) (trivial-tuple-Ring R n)))
+          ( i)
+          by refl
+        ＝ one-Ring R
+          by
+            component-tuple-with-value-identity-tuple
+              ( with-value-tuple j (neg-one-Ring R) (trivial-tuple-Ring R n))
+              ( i)
+              ( one-Ring R))
+```
+
+### An empty tuple is linearly independent
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  linearly-independent-empty-tuple-left-module-Ring :
+    tuple (type-left-module-Ring R M) zero-ℕ →
+    linearly-independent-tuple-left-module-Ring R M zero-ℕ
+  pr1 (linearly-independent-empty-tuple-left-module-Ring vectors) = vectors
+  pr2 (linearly-independent-empty-tuple-left-module-Ring vectors)
+    scalars identity = zero-empty-tuple scalars
+```
+
+### An empty subset is linearly independent
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  linearly-independent-empty-subset-left-module-Ring :
+    {l : Level} →
+    (S : subset-left-module-Ring l R M) →
+    is-empty (type-subset-left-module-Ring R M S) →
+    linearly-independent-subset-left-module-Ring l R M
+  pr1 (linearly-independent-empty-subset-left-module-Ring S empty) = S
+  pr2 (linearly-independent-empty-subset-left-module-Ring S empty)
+    zero-ℕ vectors scalars identity = zero-empty-tuple scalars
+  pr2 (linearly-independent-empty-subset-left-module-Ring S empty)
+    (succ-ℕ n) (x ∷ vectors) scalars identity = ex-falso (empty x)
+```
diff --git a/src/linear-algebra/subsets-left-modules-rings.lagda.md b/src/linear-algebra/subsets-left-modules-rings.lagda.md
index 8155bd0232..ae183dc2af 100644
--- a/src/linear-algebra/subsets-left-modules-rings.lagda.md
+++ b/src/linear-algebra/subsets-left-modules-rings.lagda.md
@@ -11,6 +11,7 @@ open import foundation.conjunction
 open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.subtypes
+open import foundation.unit-type
 open import foundation.universe-levels
 
 open import linear-algebra.left-modules-rings
@@ -51,6 +52,11 @@ module _
   inclusion-subset-left-module-Ring :
     type-subset-left-module-Ring → type-left-module-Ring R M
   inclusion-subset-left-module-Ring = pr1
+
+whole-subset-left-module-Ring :
+  {l1 l2 l3 : Level}
+  (R : Ring l1) (M : left-module-Ring l2 R) → subset-left-module-Ring l3 R M
+whole-subset-left-module-Ring R M _ = raise-unit-Prop _
 ```
 
 ### The condition that a subset is closed under addition
diff --git a/src/lists/tuples.lagda.md b/src/lists/tuples.lagda.md
index 5663fcc5b1..ccc9239825 100644
--- a/src/lists/tuples.lagda.md
+++ b/src/lists/tuples.lagda.md
@@ -18,8 +18,10 @@ open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.sets
+open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.truncated-types
 open import foundation.truncation-levels
@@ -27,6 +29,8 @@ open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-higher-homotopies-composition
 
+open import foundation-core.empty-types
+
 open import univalent-combinatorics.standard-finite-types
 ```
 
@@ -77,6 +81,11 @@ module _
   component-tuple (succ-ℕ n) (a ∷ v) (inl k) = component-tuple n v k
   component-tuple (succ-ℕ n) (a ∷ v) (inr k) = a
 
+  with-value-tuple :
+    {n : ℕ} → Fin n → A → tuple A n → tuple A n
+  with-value-tuple (inr _) a (x ∷ v) = a ∷ v
+  with-value-tuple (inl i) a (x ∷ v) = x ∷ (with-value-tuple i a v)
+
   infix 6 _∈-tuple_
   data _∈-tuple_ : {n : ℕ} → A → tuple A n → UU l where
     is-head : {n : ℕ} (a : A) (l : tuple A n) → a ∈-tuple (a ∷ l)
@@ -96,6 +105,9 @@ module _
   eq-component-tuple-index-in-tuple
     (succ-ℕ n) a (x ∷ v) (is-in-tail .a .x .v I) =
     eq-component-tuple-index-in-tuple n a v I
+
+  subset-tuple : {n : ℕ} (v : tuple A n) → subtype l A
+  subset-tuple v a = trunc-Prop (a ∈-tuple v)
 ```
 
 ## Properties
@@ -156,6 +168,15 @@ module _
 
   extensionality-tuple : (n : ℕ) → (u v : tuple A n) → Id u v ≃ Eq-tuple n u v
   extensionality-tuple n u v = (Eq-eq-tuple n u v , is-equiv-Eq-eq-tuple n u v)
+
+  elements-equal-tuple :
+    (n : ℕ) →
+    (i : Fin n) →
+    (u : tuple A n) →
+    (v : tuple A n) →
+    u ＝ v →
+    component-tuple n u i ＝ component-tuple n v i
+  elements-equal-tuple n i u v refl = refl
 ```
 
 ### The type of tuples of elements in a truncated type is truncated
@@ -251,3 +272,27 @@ compute-tr-tuple :
   (x ∷ tr (tuple A) (is-injective-succ-ℕ p) v)
 compute-tr-tuple refl v x = refl
 ```
+
+### Any tuple of length 0 is the empty tuple
+
+```agda
+zero-empty-tuple :
+  {l : Level} {A : UU l} (v : tuple A zero-ℕ) → v ＝ empty-tuple
+zero-empty-tuple empty-tuple = refl
+```
+
+### fds
+
+```agda
+component-tuple-with-value-identity-tuple :
+  {l : Level} →
+  {A : UU l} →
+  {n : ℕ}
+  (v : tuple A n) →
+  (i : Fin n) →
+  (a : A) →
+  component-tuple n (with-value-tuple i a v) i ＝ a
+component-tuple-with-value-identity-tuple (x ∷ v) (inr _) a = refl
+component-tuple-with-value-identity-tuple (x ∷ v) (inl i) a =
+  component-tuple-with-value-identity-tuple v i a
+```
diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md
index 757f7994ee..1b5fd60afc 100644
--- a/src/ring-theory/rings.lagda.md
+++ b/src/ring-theory/rings.lagda.md
@@ -28,6 +28,11 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.unital-binary-operations
 open import foundation.universe-levels
+open import foundation.negation
+
+open import foundation-core.coproduct-types
+
+open import univalent-combinatorics.standard-finite-types
 
 open import group-theory.abelian-groups
 open import group-theory.commutative-monoids
@@ -37,6 +42,7 @@ open import group-theory.semigroups
 
 open import lists.concatenation-lists
 open import lists.lists
+open import lists.tuples
 
 open import ring-theory.semirings
 ```
@@ -410,6 +416,18 @@ module _
   one-Ring : type-Ring R
   one-Ring = unit-Monoid multiplicative-monoid-Ring
 
+  zero-is-one-prop-Ring : Prop l
+  zero-is-one-prop-Ring = Id-Prop (set-Ring R) (zero-Ring R) one-Ring
+
+  zero-is-one-Ring : UU l
+  zero-is-one-Ring = type-Prop zero-is-one-prop-Ring
+
+  zero-is-not-one-prop-Ring : Prop l
+  zero-is-not-one-prop-Ring = neg-Prop zero-is-one-prop-Ring
+
+  zero-is-not-one-Ring : UU l
+  zero-is-not-one-Ring = type-Prop zero-is-not-one-prop-Ring
+
   left-unit-law-mul-Ring : (x : type-Ring R) → Id (mul-Ring R one-Ring x) x
   left-unit-law-mul-Ring = left-unit-law-mul-Monoid multiplicative-monoid-Ring
 
@@ -706,3 +724,29 @@ ring-structure-ring :
 pr1 (ring-structure-ring X (p , q)) = abelian-group-structure-abelian-group X p
 pr2 (ring-structure-ring X (p , q)) = q
 ```
+
+### Trivial tuple
+
+```agda
+trivial-tuple-Ring :
+  {l : Level} → (R : Ring l) → (n : ℕ) → tuple (type-Ring R) n
+trivial-tuple-Ring R zero-ℕ = empty-tuple
+trivial-tuple-Ring R (succ-ℕ n) =
+  zero-Ring R ∷ trivial-tuple-Ring R n
+```
+
+## Properties
+
+### Any component of the trivial tuple is the zero element
+
+```agda
+zero-component-trivial-tuple :
+  {l : Level} →
+  {R : Ring l}
+  (n : ℕ) →
+  (i : Fin n) →
+  zero-Ring R ＝ component-tuple n (trivial-tuple-Ring R n) i
+zero-component-trivial-tuple (succ-ℕ n) (inr _) = refl
+zero-component-trivial-tuple (succ-ℕ n) (inl i) =
+  zero-component-trivial-tuple n i
+```