From 83707e30f1b8750981edae4febd1923e0fdf1291 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sat, 20 Sep 2025 22:03:05 +0200
Subject: [PATCH 1/9] Add linear independence
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Šimon Brandner <simon.bra.ag@gmail.com>
---
 src/linear-algebra.lagda.md                   |   1 +
 ...les-of-vectors-left-modules-rings.lagda.md | 151 ++++++++++
 ...r-independence-left-modules-rings.lagda.md | 284 ++++++++++++++++++
 .../subsets-left-modules-rings.lagda.md       |   6 +
 src/lists/tuples.lagda.md                     |  45 +++
 src/ring-theory/rings.lagda.md                |  43 +++
 6 files changed, 530 insertions(+)
 create mode 100644 src/linear-algebra/linear-independence-left-modules-rings.lagda.md

diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index ba50e0c42c0..3a3eb9415ff 100644
--- a/src/linear-algebra.lagda.md
+++ b/src/linear-algebra.lagda.md
@@ -26,6 +26,7 @@ open import linear-algebra.left-modules-commutative-rings public
 open import linear-algebra.left-modules-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/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 acaedba8a76..bebbda8418d 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
@@ -10,6 +10,7 @@ module linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings w
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
@@ -20,6 +21,8 @@ open import lists.functoriality-tuples
 open import lists.tuples
 
 open import ring-theory.rings
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -291,3 +294,151 @@ module _
             ( vectors-b))
         by refl
 ```
+
+### Whenever the coefficient tuple is the trivial tuple, the linear combination is equal to the zero element
+
+```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)
+```
+
+### Whenever the coefficient tuple is the trivial tuple besides one value, that value determines the value of the linear combination
+
+```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 00000000000..36ea8f10a55
--- /dev/null
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -0,0 +1,284 @@
+# Linear independence
+
+```agda
+module linear-algebra.linear-independence-left-modules-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.distance-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.negation
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import foundation-core.empty-types
+open import foundation-core.sets
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings
+open import linear-algebra.subsets-left-modules-rings
+
+open import lists.concatenation-tuples
+open import lists.functoriality-tuples
+open import lists.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 8155bd02323..ae183dc2af1 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 5663fcc5b12..922164b5a21 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
+```
+
+### The value at the index of a with value call is correct
+
+```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 757f7994eec..68d523f90f2 100644
--- a/src/ring-theory/rings.lagda.md
+++ b/src/ring-theory/rings.lagda.md
@@ -29,6 +29,8 @@ open import foundation.sets
 open import foundation.unital-binary-operations
 open import foundation.universe-levels
 
+open import foundation-core.coproduct-types
+
 open import group-theory.abelian-groups
 open import group-theory.commutative-monoids
 open import group-theory.groups
@@ -37,8 +39,11 @@ open import group-theory.semigroups
 
 open import lists.concatenation-lists
 open import lists.lists
+open import lists.tuples
 
 open import ring-theory.semirings
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -410,6 +415,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 +723,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
+```

From 7f35ccddda45c446f89448337092324924ff113e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 12:45:35 +0200
Subject: [PATCH 2/9] Better title

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 .../linear-independence-left-modules-rings.lagda.md             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
index 36ea8f10a55..b1694636d06 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -131,7 +131,7 @@ module _
     type-Prop is-linearly-independent-subset-left-module-prop-Ring
 ```
 
-### Linearly independent subset of a left module over a ring
+### Linearly independent subsets of a left module over a ring
 
 ```agda
 linearly-independent-subset-left-module-Ring :

From 39a8e83cb743849b9bf439e30cd8afaed37c9df6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 12:45:45 +0200
Subject: [PATCH 3/9] Better title

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 .../linear-independence-left-modules-rings.lagda.md             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
index b1694636d06..33429fe839c 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -106,7 +106,7 @@ module _
   tuple-linearly-independent-tuple = pr1 vectors
 ```
 
-### The condition of a subset being linearly independent
+### The condition on a subset of being linearly independent
 
 ```agda
 module _

From e4624c3a89cce0c335c14ebbb2b20985dadbc551 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 12:45:53 +0200
Subject: [PATCH 4/9] Better title

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 .../linear-independence-left-modules-rings.lagda.md             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
index 33429fe839c..ef0656252c3 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -84,7 +84,7 @@ module _
     type-Prop is-linearly-independent-tuple-left-module-prop-Ring
 ```
 
-### Linearly independent tuple in a left-module over a ring
+### Linearly independent tuple in a left module over a ring
 
 ```agda
 linearly-independent-tuple-left-module-Ring :

From 38dbe0b95954fc11748656d0cc1e41dac23f46ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 12:46:09 +0200
Subject: [PATCH 5/9] Fix formatting

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 .../linear-independence-left-modules-rings.lagda.md          | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
index ef0656252c3..41e8e6af991 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -68,7 +68,7 @@ module _
   is-linearly-independent-tuple-left-module-prop-Ring =
     Π-Prop
       ( tuple (type-Ring R) n)
-      λ scalars →
+      ( λ scalars →
         hom-Prop
           ( Id-Prop
             ( set-left-module-Ring R M)
@@ -77,8 +77,7 @@ module _
           ( Id-Prop
             ( tuple-Set (set-Ring R) n)
             ( scalars)
-            ( trivial-tuple-Ring R n))
-
+            ( 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

From caa36f337eb5727c508a8a78ab3c18ebd7d41d87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 13:58:41 +0200
Subject: [PATCH 6/9] Remove subset tuple
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Šimon Brandner <simon.bra.ag@gmail.com>
---
 src/lists/tuples.lagda.md | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/lists/tuples.lagda.md b/src/lists/tuples.lagda.md
index 922164b5a21..afd8729259a 100644
--- a/src/lists/tuples.lagda.md
+++ b/src/lists/tuples.lagda.md
@@ -105,9 +105,6 @@ 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

From 10a5f4120a1b7f2c16206f48b2e49eb31b955acb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 13:59:56 +0200
Subject: [PATCH 7/9] Better name
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Šimon Brandner <simon.bra.ag@gmail.com>
---
 .../linear-independence-left-modules-rings.lagda.md           | 2 +-
 src/lists/tuples.lagda.md                                     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
index 41e8e6af991..59c6fb44ef0 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -210,7 +210,7 @@ module _
               ( j))
             ( i)
           by
-            elements-equal-tuple
+            eq-component-eq-tuple
               ( n)
               ( i)
               ( trivial-tuple-Ring R n)
diff --git a/src/lists/tuples.lagda.md b/src/lists/tuples.lagda.md
index afd8729259a..3801b6f8703 100644
--- a/src/lists/tuples.lagda.md
+++ b/src/lists/tuples.lagda.md
@@ -166,14 +166,14 @@ 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 :
+  eq-component-eq-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
+  eq-component-eq-tuple n i u v refl = refl
 ```
 
 ### The type of tuples of elements in a truncated type is truncated

From 2d00193b3968e9aee2dfa3b5efa6caba20096756 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 15:10:49 +0200
Subject: [PATCH 8/9] Remove duplicate definition
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Šimon Brandner <simon.bra.ag@gmail.com>
---
 .../linear-independence-left-modules-rings.lagda.md  |  3 ++-
 src/ring-theory/rings.lagda.md                       | 12 ------------
 2 files changed, 2 insertions(+), 13 deletions(-)

diff --git a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
index 59c6fb44ef0..9ead45fb19a 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -32,6 +32,7 @@ open import lists.functoriality-tuples
 open import lists.tuples
 
 open import ring-theory.rings
+open import ring-theory.trivial-rings
 
 open import univalent-combinatorics.standard-finite-types
 ```
@@ -189,7 +190,7 @@ module _
     {! !}
 
   linearly-dependent-repeated-element-tuple-left-module-Ring :
-    (zero-is-not-one-Ring R) →
+    (is-nontrivial-Ring R) →
     (n : ℕ) →
     (vectors : tuple (type-left-module-Ring R M) n) →
     (i j : Fin n) →
diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md
index 68d523f90f2..106cf18fd64 100644
--- a/src/ring-theory/rings.lagda.md
+++ b/src/ring-theory/rings.lagda.md
@@ -415,18 +415,6 @@ 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
 

From 990b3033c323ded75aaa93f022aa21d6aceb76c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=A0imon=20Brandner?= <simon.bra.ag@gmail.com>
Date: Sun, 21 Sep 2025 19:03:00 +0200
Subject: [PATCH 9/9] Move tuples in rings to its own file
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Šimon Brandner <simon.bra.ag@gmail.com>
---
 ...les-of-vectors-left-modules-rings.lagda.md | 33 ++++++------
 ...r-independence-left-modules-rings.lagda.md | 15 +++---
 src/ring-theory/rings.lagda.md                | 26 ----------
 src/ring-theory/tuples-in-rings.lagda.md      | 52 +++++++++++++++++++
 4 files changed, 77 insertions(+), 49 deletions(-)
 create mode 100644 src/ring-theory/tuples-in-rings.lagda.md

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 bebbda8418d..f9c6fca7c78 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
@@ -21,6 +21,7 @@ open import lists.functoriality-tuples
 open import lists.tuples
 
 open import ring-theory.rings
+open import ring-theory.tuples-in-rings
 
 open import univalent-combinatorics.standard-finite-types
 ```
@@ -308,7 +309,7 @@ module _
     (n : ℕ) →
     (vectors : tuple (type-left-module-Ring R M) n) →
     linear-combination-tuple-left-module-Ring R M
-      ( trivial-tuple-Ring R n)
+      ( zero-tuple-type-Ring R n)
       ( vectors) ＝
     zero-left-module-Ring R M
   zero-trivial-tuple-linear-combination-tuple-left-module-Ring n empty-tuple =
@@ -317,24 +318,24 @@ module _
     (succ-ℕ n) (x ∷ vectors) =
     equational-reasoning
     linear-combination-tuple-left-module-Ring R M
-      ( zero-Ring R ∷ trivial-tuple-Ring R n)
+      ( zero-Ring R ∷ zero-tuple-type-Ring R n)
       ( x ∷ vectors)
     ＝ add-left-module-Ring R M
       ( linear-combination-tuple-left-module-Ring R M
-        ( trivial-tuple-Ring R n)
+        ( zero-tuple-type-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)
+        ( zero-tuple-type-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)
+              ( zero-tuple-type-Ring R n)
               ( vectors))
             ( y))
           (left-zero-law-mul-left-module-Ring R M x)
@@ -365,22 +366,22 @@ module _
     (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))
+      ( with-value-tuple i r (zero-tuple-type-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)))
+      ( with-value-tuple (inr _) r (zero-tuple-type-Ring R (succ-ℕ n)))
       ( x ∷ vectors)
     ＝ linear-combination-tuple-left-module-Ring R M
-      ( r ∷ (trivial-tuple-Ring R n))
+      ( r ∷ (zero-tuple-type-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)
+        ( zero-tuple-type-Ring R n)
         ( vectors))
       ( mul-left-module-Ring R M r x)
       by refl
@@ -401,37 +402,37 @@ module _
     (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)))
+      ( with-value-tuple (inl i) r (zero-tuple-type-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)))
+      ( zero-Ring R ∷ (with-value-tuple i r (zero-tuple-type-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))
+        ( with-value-tuple i r (zero-tuple-type-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))
+        ( with-value-tuple i r (zero-tuple-type-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))
+              ( with-value-tuple i r (zero-tuple-type-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))
+        ( with-value-tuple i r (zero-tuple-type-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))
+          ( with-value-tuple i r (zero-tuple-type-Ring R n))
           ( vectors))
     ＝ mul-left-module-Ring R M r
       ( component-tuple (succ-ℕ n) (x ∷ vectors) (inl 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
index 9ead45fb19a..355bdda567b 100644
--- a/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
+++ b/src/linear-algebra/linear-independence-left-modules-rings.lagda.md
@@ -33,6 +33,7 @@ open import lists.tuples
 
 open import ring-theory.rings
 open import ring-theory.trivial-rings
+open import ring-theory.tuples-in-rings
 
 open import univalent-combinatorics.standard-finite-types
 ```
@@ -78,7 +79,7 @@ module _
           ( Id-Prop
             ( tuple-Set (set-Ring R) n)
             ( scalars)
-            ( trivial-tuple-Ring R n)))
+            ( zero-tuple-type-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
@@ -170,7 +171,7 @@ module _
     n i j =
     ( with-value-tuple i
       ( one-Ring R)
-      ( with-value-tuple j (neg-one-Ring R) (trivial-tuple-Ring R n)))
+      ( with-value-tuple j (neg-one-Ring R) (zero-tuple-type-Ring R n)))
 
   gives-zero-linearly-dependent-repeated-element-tuple :
     (n : ℕ) →
@@ -202,8 +203,8 @@ module _
     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 (zero-tuple-type-Ring R n) i
+          by zero-component-zero-tuple-type-Ring n i
         ＝ component-tuple n
             ( non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring
               ( n)
@@ -214,7 +215,7 @@ module _
             eq-component-eq-tuple
               ( n)
               ( i)
-              ( trivial-tuple-Ring R n)
+              ( zero-tuple-type-Ring R n)
               ( non-trivial-tuple-linearly-dependent-repeated-element-tuple-left-module-Ring
                 ( n)
                 ( i)
@@ -234,13 +235,13 @@ module _
                     ( identity))))
         ＝ component-tuple n
           ( with-value-tuple i (one-Ring R)
-            ( with-value-tuple j (neg-one-Ring R) (trivial-tuple-Ring R n)))
+            ( with-value-tuple j (neg-one-Ring R) (zero-tuple-type-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))
+              ( with-value-tuple j (neg-one-Ring R) (zero-tuple-type-Ring R n))
               ( i)
               ( one-Ring R))
 ```
diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md
index 106cf18fd64..0150a933230 100644
--- a/src/ring-theory/rings.lagda.md
+++ b/src/ring-theory/rings.lagda.md
@@ -711,29 +711,3 @@ 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
-```
diff --git a/src/ring-theory/tuples-in-rings.lagda.md b/src/ring-theory/tuples-in-rings.lagda.md
new file mode 100644
index 00000000000..5563697e9ef
--- /dev/null
+++ b/src/ring-theory/tuples-in-rings.lagda.md
@@ -0,0 +1,52 @@
+# Tuples in rings
+
+```agda
+module ring-theory.tuples-in-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import foundation-core.coproduct-types
+
+open import lists.tuples
+
+open import ring-theory.rings
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Definitions
+
+### Zero tuple
+
+```agda
+zero-tuple-type-Ring :
+  {l : Level} → (R : Ring l) → (n : ℕ) → tuple (type-Ring R) n
+zero-tuple-type-Ring R zero-ℕ = empty-tuple
+zero-tuple-type-Ring R (succ-ℕ n) =
+  zero-Ring R ∷ zero-tuple-type-Ring R n
+```
+
+## Properties
+
+### Any component of the zero tuple is the zero element
+
+```agda
+zero-component-zero-tuple-type-Ring :
+  {l : Level} →
+  {R : Ring l}
+  (n : ℕ) →
+  (i : Fin n) →
+  zero-Ring R ＝ component-tuple n (zero-tuple-type-Ring R n) i
+zero-component-zero-tuple-type-Ring (succ-ℕ n) (inr _) = refl
+zero-component-zero-tuple-type-Ring (succ-ℕ n) (inl i) =
+  zero-component-zero-tuple-type-Ring n i
+```