diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md
index db76ba0076..d56e4effe8 100644
--- a/src/commutative-algebra.lagda.md
+++ b/src/commutative-algebra.lagda.md
@@ -22,6 +22,8 @@ open import commutative-algebra.formal-power-series-commutative-semirings public
 open import commutative-algebra.full-ideals-commutative-rings public
 open import commutative-algebra.function-commutative-rings public
 open import commutative-algebra.function-commutative-semirings public
+open import commutative-algebra.geometric-sequences-commutative-rings public
+open import commutative-algebra.geometric-sequences-commutative-semirings public
 open import commutative-algebra.groups-of-units-commutative-rings public
 open import commutative-algebra.homomorphisms-commutative-rings public
 open import commutative-algebra.homomorphisms-commutative-semirings public
diff --git a/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md
new file mode 100644
index 0000000000..9343e05ed8
--- /dev/null
+++ b/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md
@@ -0,0 +1,310 @@
+# Geometric sequences in commutative rings
+
+```agda
+module commutative-algebra.geometric-sequences-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+open import commutative-algebra.commutative-semirings
+open import commutative-algebra.geometric-sequences-commutative-semirings
+open import commutative-algebra.powers-of-elements-commutative-rings
+
+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.binary-transport
+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.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.arithmetic-sequences-semigroups
+
+open import lists.finite-sequences
+open import lists.sequences
+```
+
+</details>
+
+## Ideas
+
+A
+{{#concept "geometric sequence" Disambiguation="in a commutative ring" Agda=geometric-sequence-Commutative-Ring}}
+in a [commutative ring](commutative-algebra.commutative-rings.md) is an
+[geometric sequence](ring-theory.geometric-sequences-semirings.md) in the ring's
+multiplicative [semigroup](group-theory.semigroups.md).
+
+These are sequences of the form `n ↦ a * rⁿ`, for elements `a`, `r` in the ring.
+
+## Definitions
+
+### Geometric sequences in commutative rings
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  where
+
+  geometric-sequence-Commutative-Ring : UU l
+  geometric-sequence-Commutative-Ring =
+    geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+
+  is-geometric-sequence-Commutative-Ring :
+    sequence (type-Commutative-Ring R) → UU l
+  is-geometric-sequence-Commutative-Ring =
+    is-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+
+module _
+  {l : Level} (R : Commutative-Ring l)
+  (u : geometric-sequence-Commutative-Ring R)
+  where
+
+  seq-geometric-sequence-Commutative-Ring : ℕ → type-Commutative-Ring R
+  seq-geometric-sequence-Commutative-Ring =
+    seq-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+
+  is-geometric-seq-geometric-sequence-Commutative-Ring :
+    is-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( seq-geometric-sequence-Commutative-Ring)
+  is-geometric-seq-geometric-sequence-Commutative-Ring =
+    is-geometric-seq-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+
+  common-ratio-geometric-sequence-Commutative-Ring :
+    type-Commutative-Ring R
+  common-ratio-geometric-sequence-Commutative-Ring =
+    common-ratio-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+
+  is-common-ratio-geometric-sequence-Commutative-Ring :
+    ( n : ℕ) →
+    ( seq-geometric-sequence-Commutative-Ring (succ-ℕ n)) ＝
+    ( mul-Commutative-Ring
+      ( R)
+      ( seq-geometric-sequence-Commutative-Ring n)
+      ( common-ratio-geometric-sequence-Commutative-Ring))
+  is-common-ratio-geometric-sequence-Commutative-Ring =
+    is-common-ratio-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+
+  initial-term-geometric-sequence-Commutative-Ring :
+    type-Commutative-Ring R
+  initial-term-geometric-sequence-Commutative-Ring =
+    initial-term-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+```
+
+### The standard geometric sequences in a commutative ring
+
+The standard geometric sequence with initial term `a` and common factor `r` is
+the sequence `u` defined by:
+
+- `u₀ = a`
+- `uₙ₊₁ = uₙ * r`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  where
+
+  standard-geometric-sequence-Commutative-Ring :
+    geometric-sequence-Commutative-Ring R
+  standard-geometric-sequence-Commutative-Ring =
+    standard-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( a)
+      ( r)
+
+  seq-standard-geometric-sequence-Commutative-Ring :
+    ℕ → type-Commutative-Ring R
+  seq-standard-geometric-sequence-Commutative-Ring =
+    seq-geometric-sequence-Commutative-Ring R
+      standard-geometric-sequence-Commutative-Ring
+
+  is-geometric-standard-geometric-sequence-Commutative-Ring :
+    is-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( seq-standard-geometric-sequence-Commutative-Ring)
+  is-geometric-standard-geometric-sequence-Commutative-Ring =
+    is-geometric-seq-geometric-sequence-Commutative-Ring R
+      standard-geometric-sequence-Commutative-Ring
+```
+
+### The geometric sequences `n ↦ a * rⁿ`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  where
+
+  mul-pow-nat-Commutative-Ring : ℕ → type-Commutative-Ring R
+  mul-pow-nat-Commutative-Ring n =
+    mul-Commutative-Ring R a (power-Commutative-Ring R n r)
+
+  geometric-mul-pow-nat-Commutative-Ring : geometric-sequence-Commutative-Ring R
+  geometric-mul-pow-nat-Commutative-Ring =
+    geometric-mul-pow-nat-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( a)
+      ( r)
+
+  initial-term-mul-pow-nat-Commutative-Ring : type-Commutative-Ring R
+  initial-term-mul-pow-nat-Commutative-Ring =
+    initial-term-geometric-sequence-Commutative-Ring
+      ( R)
+      ( geometric-mul-pow-nat-Commutative-Ring)
+
+  eq-initial-term-mul-pow-nat-Commutative-Ring :
+    initial-term-mul-pow-nat-Commutative-Ring ＝ a
+  eq-initial-term-mul-pow-nat-Commutative-Ring =
+    right-unit-law-mul-Commutative-Ring R a
+```
+
+## Properties
+
+### Any geometric sequence is homotopic to a standard geometric sequence
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  (u : geometric-sequence-Commutative-Ring R)
+  where
+
+  htpy-seq-standard-geometric-sequence-Commutative-Ring :
+    ( seq-geometric-sequence-Commutative-Ring R
+      ( standard-geometric-sequence-Commutative-Ring R
+        ( initial-term-geometric-sequence-Commutative-Ring R u)
+        ( common-ratio-geometric-sequence-Commutative-Ring R u))) ~
+    ( seq-geometric-sequence-Commutative-Ring R u)
+  htpy-seq-standard-geometric-sequence-Commutative-Ring =
+    htpy-seq-standard-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+```
+
+### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  where
+
+  htpy-mul-pow-standard-geometric-sequence-Commutative-Ring :
+    mul-pow-nat-Commutative-Ring R a r ~
+    seq-standard-geometric-sequence-Commutative-Ring R a r
+  htpy-mul-pow-standard-geometric-sequence-Commutative-Ring =
+    htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( a)
+      ( r)
+
+  initial-term-standard-geometric-sequence-Commutative-Ring :
+    seq-standard-geometric-sequence-Commutative-Ring R a r 0 ＝ a
+  initial-term-standard-geometric-sequence-Commutative-Ring =
+    ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Ring 0)) ∙
+    ( eq-initial-term-mul-pow-nat-Commutative-Ring R a r)
+```
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  (u : geometric-sequence-Commutative-Ring R)
+  where
+
+  htpy-mul-pow-geometric-sequence-Commutative-Ring :
+    mul-pow-nat-Commutative-Ring
+      ( R)
+      ( initial-term-geometric-sequence-Commutative-Ring R u)
+      ( common-ratio-geometric-sequence-Commutative-Ring R u) ~
+    seq-geometric-sequence-Commutative-Ring R u
+  htpy-mul-pow-geometric-sequence-Commutative-Ring n =
+    ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
+      ( R)
+      ( initial-term-geometric-sequence-Commutative-Ring R u)
+      ( common-ratio-geometric-sequence-Commutative-Ring R u)
+      ( n)) ∙
+    ( htpy-seq-standard-geometric-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( u)
+      ( n))
+```
+
+### Constant sequences are geometric with common ratio one
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l) (a : type-Commutative-Ring R)
+  where
+
+  geometric-const-sequence-Commutative-Ring :
+    geometric-sequence-Commutative-Ring R
+  geometric-const-sequence-Commutative-Ring =
+    geometric-const-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( a)
+```
+
+### Finite geometric sequences
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  where
+
+  standard-geometric-fin-sequence-Commutative-Ring :
+    (n : ℕ) → fin-sequence (type-Commutative-Ring R) n
+  standard-geometric-fin-sequence-Commutative-Ring =
+    fin-sequence-sequence
+      ( seq-standard-geometric-sequence-Commutative-Ring R a r)
+
+  sum-standard-geometric-fin-sequence-Commutative-Ring :
+    (n : ℕ) → type-Commutative-Ring R
+  sum-standard-geometric-fin-sequence-Commutative-Ring =
+    sum-standard-geometric-fin-sequence-Commutative-Semiring
+      ( commutative-semiring-Commutative-Ring R)
+      ( a)
+      ( r)
+```
+
+### The sum of a finite geometric sequence
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  where
+
+  abstract
+    compute-sum-standard-geometric-fin-sequence-succ-Commutative-Ring :
+      (n : ℕ) →
+      sum-standard-geometric-fin-sequence-Commutative-Ring R
+        ( a)
+        ( r)
+        ( succ-ℕ n) ＝
+      add-Commutative-Ring R
+        ( a)
+        ( mul-Commutative-Ring R
+          ( r)
+          ( sum-standard-geometric-fin-sequence-Commutative-Ring R a r n))
+    compute-sum-standard-geometric-fin-sequence-succ-Commutative-Ring =
+      compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring
+        ( commutative-semiring-Commutative-Ring R)
+        ( a)
+        ( r)
+```
diff --git a/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md
new file mode 100644
index 0000000000..1e4b7ed9f9
--- /dev/null
+++ b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md
@@ -0,0 +1,446 @@
+# Geometric sequences in commutative semirings
+
+```agda
+module commutative-algebra.geometric-sequences-commutative-semirings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-semirings
+open import commutative-algebra.powers-of-elements-commutative-semirings
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semirings
+
+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.binary-transport
+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.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.arithmetic-sequences-semigroups
+
+open import lists.finite-sequences
+open import lists.sequences
+
+open import ring-theory.geometric-sequences-semirings
+open import ring-theory.powers-of-elements-semirings
+open import ring-theory.semirings
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Ideas
+
+A
+{{#concept "geometric sequence" Disambiguation="in a commutative semiring" Agda=geometric-sequence-Commutative-Semiring}}
+in a [commutative semiring](commutative-algebra.commutative-semirings.md) is an
+[geometric sequence](ring-theory.geometric-sequences-semirings.md) in the
+semiring's multiplicative [semigroup](group-theory.semigroups.md).
+
+These are sequences of the form `n ↦ a * rⁿ`, for elements `a`, `r` in the
+semiring.
+
+## Definitions
+
+### Geometric sequences in commutative semirings
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l)
+  where
+
+  geometric-sequence-Commutative-Semiring : UU l
+  geometric-sequence-Commutative-Semiring =
+    geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+
+  is-geometric-sequence-Commutative-Semiring :
+    sequence (type-Commutative-Semiring R) → UU l
+  is-geometric-sequence-Commutative-Semiring =
+    is-geometric-sequence-Semiring (semiring-Commutative-Semiring R)
+
+module _
+  {l : Level} (R : Commutative-Semiring l)
+  (u : geometric-sequence-Commutative-Semiring R)
+  where
+
+  seq-geometric-sequence-Commutative-Semiring : ℕ → type-Commutative-Semiring R
+  seq-geometric-sequence-Commutative-Semiring =
+    seq-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+
+  is-geometric-seq-geometric-sequence-Commutative-Semiring :
+    is-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( seq-geometric-sequence-Commutative-Semiring)
+  is-geometric-seq-geometric-sequence-Commutative-Semiring =
+    is-geometric-seq-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+
+  common-ratio-geometric-sequence-Commutative-Semiring :
+    type-Commutative-Semiring R
+  common-ratio-geometric-sequence-Commutative-Semiring =
+    common-ratio-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+
+  is-common-ratio-geometric-sequence-Commutative-Semiring :
+    ( n : ℕ) →
+    ( seq-geometric-sequence-Commutative-Semiring (succ-ℕ n)) ＝
+    ( mul-Commutative-Semiring
+      ( R)
+      ( seq-geometric-sequence-Commutative-Semiring n)
+      ( common-ratio-geometric-sequence-Commutative-Semiring))
+  is-common-ratio-geometric-sequence-Commutative-Semiring =
+    is-common-ratio-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+
+  initial-term-geometric-sequence-Commutative-Semiring :
+    type-Commutative-Semiring R
+  initial-term-geometric-sequence-Commutative-Semiring =
+    initial-term-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+```
+
+### The standard geometric sequences in a commutative semiring
+
+The standard geometric sequence with initial term `a` and common factor `r` is
+the sequence `u` defined by:
+
+- `u₀ = a`
+- `uₙ₊₁ = uₙ * r`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R)
+  where
+
+  standard-geometric-sequence-Commutative-Semiring :
+    geometric-sequence-Commutative-Semiring R
+  standard-geometric-sequence-Commutative-Semiring =
+    standard-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( a)
+      ( r)
+
+  seq-standard-geometric-sequence-Commutative-Semiring :
+    ℕ → type-Commutative-Semiring R
+  seq-standard-geometric-sequence-Commutative-Semiring =
+    seq-geometric-sequence-Commutative-Semiring R
+      standard-geometric-sequence-Commutative-Semiring
+
+  is-geometric-standard-geometric-sequence-Commutative-Semiring :
+    is-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( seq-standard-geometric-sequence-Commutative-Semiring)
+  is-geometric-standard-geometric-sequence-Commutative-Semiring =
+    is-geometric-seq-geometric-sequence-Commutative-Semiring R
+      standard-geometric-sequence-Commutative-Semiring
+```
+
+### The geometric sequences `n ↦ a * rⁿ`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R)
+  where
+
+  mul-pow-nat-Commutative-Semiring : ℕ → type-Commutative-Semiring R
+  mul-pow-nat-Commutative-Semiring n =
+    mul-Commutative-Semiring R a (power-Commutative-Semiring R n r)
+
+  geometric-mul-pow-nat-Commutative-Semiring :
+    geometric-sequence-Commutative-Semiring R
+  geometric-mul-pow-nat-Commutative-Semiring =
+    geometric-mul-pow-nat-Semiring (semiring-Commutative-Semiring R) a r
+
+  initial-term-mul-pow-nat-Commutative-Semiring : type-Commutative-Semiring R
+  initial-term-mul-pow-nat-Commutative-Semiring =
+    initial-term-geometric-sequence-Commutative-Semiring
+      ( R)
+      ( geometric-mul-pow-nat-Commutative-Semiring)
+
+  eq-initial-term-mul-pow-nat-Commutative-Semiring :
+    initial-term-mul-pow-nat-Commutative-Semiring ＝ a
+  eq-initial-term-mul-pow-nat-Commutative-Semiring =
+    right-unit-law-mul-Commutative-Semiring R a
+```
+
+## Properties
+
+### Any geometric sequence is homotopic to a standard geometric sequence
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l)
+  (u : geometric-sequence-Commutative-Semiring R)
+  where
+
+  htpy-seq-standard-geometric-sequence-Commutative-Semiring :
+    ( seq-geometric-sequence-Commutative-Semiring R
+      ( standard-geometric-sequence-Commutative-Semiring R
+        ( initial-term-geometric-sequence-Commutative-Semiring R u)
+        ( common-ratio-geometric-sequence-Commutative-Semiring R u))) ~
+    ( seq-geometric-sequence-Commutative-Semiring R u)
+  htpy-seq-standard-geometric-sequence-Commutative-Semiring =
+    htpy-seq-standard-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+```
+
+### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R)
+  where
+
+  htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring :
+    mul-pow-nat-Commutative-Semiring R a r ~
+    seq-standard-geometric-sequence-Commutative-Semiring R a r
+  htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring =
+    htpy-mul-pow-standard-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( a)
+      ( r)
+
+  initial-term-standard-geometric-sequence-Commutative-Semiring :
+    seq-standard-geometric-sequence-Commutative-Semiring R a r 0 ＝ a
+  initial-term-standard-geometric-sequence-Commutative-Semiring =
+    ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring 0)) ∙
+    ( eq-initial-term-mul-pow-nat-Commutative-Semiring R a r)
+```
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l)
+  (u : geometric-sequence-Commutative-Semiring R)
+  where
+
+  htpy-mul-pow-geometric-sequence-Commutative-Semiring :
+    mul-pow-nat-Commutative-Semiring
+      ( R)
+      ( initial-term-geometric-sequence-Commutative-Semiring R u)
+      ( common-ratio-geometric-sequence-Commutative-Semiring R u) ~
+    seq-geometric-sequence-Commutative-Semiring R u
+  htpy-mul-pow-geometric-sequence-Commutative-Semiring n =
+    ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+      ( R)
+      ( initial-term-geometric-sequence-Commutative-Semiring R u)
+      ( common-ratio-geometric-sequence-Commutative-Semiring R u)
+      ( n)) ∙
+    ( htpy-seq-standard-geometric-sequence-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( u)
+      ( n))
+```
+
+### Constant sequences are geometric with common ratio one
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l) (a : type-Commutative-Semiring R)
+  where
+
+  geometric-const-sequence-Commutative-Semiring :
+    geometric-sequence-Commutative-Semiring R
+  geometric-const-sequence-Commutative-Semiring =
+    geometric-const-sequence-Semiring (semiring-Commutative-Semiring R) a
+```
+
+### Finite geometric sequences
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R)
+  where
+
+  standard-geometric-fin-sequence-Commutative-Semiring :
+    (n : ℕ) → fin-sequence (type-Commutative-Semiring R) n
+  standard-geometric-fin-sequence-Commutative-Semiring =
+    fin-sequence-sequence
+      ( seq-standard-geometric-sequence-Commutative-Semiring R a r)
+
+  sum-standard-geometric-fin-sequence-Commutative-Semiring :
+    (n : ℕ) → type-Commutative-Semiring R
+  sum-standard-geometric-fin-sequence-Commutative-Semiring n =
+    sum-fin-sequence-type-Commutative-Semiring R n
+      ( standard-geometric-fin-sequence-Commutative-Semiring n)
+```
+
+### The sum of a finite geometric sequence
+
+```agda
+module _
+  {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R)
+  where
+
+  abstract
+    compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring :
+      (n : ℕ) →
+      sum-standard-geometric-fin-sequence-Commutative-Semiring R
+        ( a)
+        ( r)
+        ( succ-ℕ n) ＝
+      add-Commutative-Semiring R
+        ( a)
+        ( mul-Commutative-Semiring R
+          ( r)
+          ( sum-standard-geometric-fin-sequence-Commutative-Semiring R a r n))
+    compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring n =
+      equational-reasoning
+        sum-standard-geometric-fin-sequence-Commutative-Semiring R
+          ( a)
+          ( r)
+          ( succ-ℕ n)
+        ＝
+          add-Commutative-Semiring R
+            ( standard-geometric-fin-sequence-Commutative-Semiring R
+              ( a)
+              ( r)
+              ( succ-ℕ n)
+              ( zero-Fin n))
+            ( sum-fin-sequence-type-Commutative-Semiring R n
+              ( λ i →
+                standard-geometric-fin-sequence-Commutative-Semiring R
+                  ( a)
+                  ( r)
+                  ( succ-ℕ n)
+                  ( inr-Fin n i)))
+          by
+            snoc-sum-fin-sequence-type-Commutative-Semiring R n
+              ( standard-geometric-fin-sequence-Commutative-Semiring R
+                ( a)
+                ( r)
+                ( succ-ℕ n))
+              ( refl)
+        ＝
+          add-Commutative-Semiring R
+            ( seq-standard-geometric-sequence-Commutative-Semiring R a r 0)
+            ( sum-fin-sequence-type-Commutative-Semiring R n
+              ( λ i →
+                seq-standard-geometric-sequence-Commutative-Semiring R
+                  ( a)
+                  ( r)
+                  ( succ-ℕ (nat-Fin n i))))
+          by
+            ap-add-Commutative-Semiring R
+              ( ap
+                ( seq-standard-geometric-sequence-Commutative-Semiring R a r)
+                ( is-zero-nat-zero-Fin {n}))
+              ( htpy-sum-fin-sequence-type-Commutative-Semiring R n
+                ( λ i →
+                  ap
+                    ( seq-standard-geometric-sequence-Commutative-Semiring R
+                      ( a)
+                      ( r))
+                    ( nat-inr-Fin n i)))
+        ＝
+          add-Commutative-Semiring R
+            ( a)
+            ( sum-fin-sequence-type-Commutative-Semiring R n
+              ( λ i →
+                mul-Commutative-Semiring R
+                  ( a)
+                  ( power-Commutative-Semiring R (succ-ℕ (nat-Fin n i)) r)))
+            by
+              ap-add-Commutative-Semiring R
+                ( initial-term-standard-geometric-sequence-Commutative-Semiring
+                  ( R)
+                  ( a)
+                  ( r))
+                ( htpy-sum-fin-sequence-type-Commutative-Semiring R n
+                  ( λ i →
+                    inv
+                      ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+                        ( R)
+                        ( a)
+                        ( r)
+                        ( succ-ℕ (nat-Fin n i)))))
+        ＝
+          add-Commutative-Semiring R
+            ( a)
+            ( sum-fin-sequence-type-Commutative-Semiring R n
+              ( λ i →
+                mul-Commutative-Semiring R
+                  ( a)
+                  ( mul-Commutative-Semiring R
+                    ( r)
+                    ( power-Commutative-Semiring R (nat-Fin n i) r))))
+            by
+              ap-add-Commutative-Semiring R
+                ( refl)
+                ( htpy-sum-fin-sequence-type-Commutative-Semiring R n
+                  ( λ i →
+                    ap-mul-Commutative-Semiring R
+                      ( refl)
+                      ( power-succ-Commutative-Semiring' R (nat-Fin n i) r)))
+        ＝
+          add-Commutative-Semiring R
+            ( a)
+            ( sum-fin-sequence-type-Commutative-Semiring R n
+              ( λ i →
+                mul-Commutative-Semiring R
+                  ( r)
+                  ( mul-Commutative-Semiring R
+                    ( a)
+                    ( power-Commutative-Semiring R (nat-Fin n i) r))))
+            by
+              ap-add-Commutative-Semiring R
+                ( refl)
+                ( htpy-sum-fin-sequence-type-Commutative-Semiring R n
+                  ( λ i → left-swap-mul-Commutative-Semiring R _ _ _))
+        ＝
+          add-Commutative-Semiring R
+            ( a)
+            ( mul-Commutative-Semiring R
+              ( r)
+              ( sum-fin-sequence-type-Commutative-Semiring R n
+                ( λ i →
+                  mul-Commutative-Semiring R
+                    ( a)
+                    ( power-Commutative-Semiring R (nat-Fin n i) r))))
+          by
+            ap-add-Commutative-Semiring R
+              ( refl)
+              ( inv
+                ( left-distributive-mul-sum-fin-sequence-type-Commutative-Semiring
+                  ( R)
+                  ( n)
+                  ( r)
+                  ( _)))
+        ＝
+          add-Commutative-Semiring R
+            ( a)
+            ( mul-Commutative-Semiring R
+              ( r)
+              ( sum-standard-geometric-fin-sequence-Commutative-Semiring R
+                ( a)
+                ( r)
+                ( n)))
+          by
+            ap-add-Commutative-Semiring R
+              ( refl)
+              ( ap-mul-Commutative-Semiring R
+                ( refl)
+                ( htpy-sum-fin-sequence-type-Commutative-Semiring R n
+                  ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+                      ( R)
+                      ( a)
+                      ( r) ∘
+                    nat-Fin n)))
+```
diff --git a/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md b/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md
index 0bda772d1a..a5727d03a8 100644
--- a/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md
+++ b/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md
@@ -51,6 +51,21 @@ module _
     power-succ-Semiring (semiring-Commutative-Semiring A)
 ```
 
+### `xⁿ⁺¹ = xxⁿ`
+
+```agda
+module _
+  {l : Level} (A : Commutative-Semiring l)
+  where
+
+  power-succ-Commutative-Semiring' :
+    (n : ℕ) (x : type-Commutative-Semiring A) →
+    power-Commutative-Semiring A (succ-ℕ n) x ＝
+    mul-Commutative-Semiring A x (power-Commutative-Semiring A n x)
+  power-succ-Commutative-Semiring' =
+    power-succ-Semiring' (semiring-Commutative-Semiring A)
+```
+
 ### Powers by sums of natural numbers are products of powers
 
 ```agda
diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index bb74acf279..9177a7585e 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -85,6 +85,7 @@ open import elementary-number-theory.finitary-natural-numbers public
 open import elementary-number-theory.finitely-cyclic-maps public
 open import elementary-number-theory.fundamental-theorem-of-arithmetic public
 open import elementary-number-theory.geometric-sequences-positive-rational-numbers public
+open import elementary-number-theory.geometric-sequences-rational-numbers public
 open import elementary-number-theory.goldbach-conjecture public
 open import elementary-number-theory.greatest-common-divisor-integers public
 open import elementary-number-theory.greatest-common-divisor-natural-numbers public
diff --git a/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md
new file mode 100644
index 0000000000..d59c56016e
--- /dev/null
+++ b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md
@@ -0,0 +1,203 @@
+# Geometric sequences of rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.geometric-sequences-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.geometric-sequences-commutative-rings
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
+
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.multiplicative-group-of-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.powers-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.ring-of-rational-numbers
+
+open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.universe-levels
+
+open import group-theory.groups
+
+open import lists.sequences
+
+open import order-theory.strictly-increasing-sequences-strictly-preordered-sets
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "geometric sequence" Disambiguation="of rational numbers" Agda=geometric-sequence-ℚ}}
+of [rational numbers](elementary-number-theory.positive-rational-numbers.md) is
+a
+[geometric sequence](commutative-algebra.geometric-sequences-commutative-rings.md)
+in the
+[commutative ring of rational numbers](elementary-number-theory.ring-of-rational-numbers.md).
+
+## Definitions
+
+```agda
+geometric-sequence-ℚ : UU lzero
+geometric-sequence-ℚ = geometric-sequence-Commutative-Ring commutative-ring-ℚ
+
+seq-geometric-sequence-ℚ : geometric-sequence-ℚ → sequence ℚ
+seq-geometric-sequence-ℚ =
+  seq-geometric-sequence-Commutative-Ring commutative-ring-ℚ
+
+standard-geometric-sequence-ℚ : ℚ → ℚ → geometric-sequence-ℚ
+standard-geometric-sequence-ℚ =
+  standard-geometric-sequence-Commutative-Ring commutative-ring-ℚ
+
+seq-standard-geometric-sequence-ℚ : ℚ → ℚ → sequence ℚ
+seq-standard-geometric-sequence-ℚ =
+  seq-standard-geometric-sequence-Commutative-Ring commutative-ring-ℚ
+```
+
+## Properties
+
+### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
+
+```agda
+module _
+  (a r : ℚ)
+  where
+
+  compute-standard-geometric-sequence-ℚ :
+    (n : ℕ) → seq-standard-geometric-sequence-ℚ a r n ＝ a *ℚ power-ℚ n r
+  compute-standard-geometric-sequence-ℚ n =
+    inv
+      ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
+        ( commutative-ring-ℚ)
+        ( a)
+        ( r)
+        ( n))
+```
+
+### If `r ≠ 1`, the sum of the first `n` elements of the standard geometric sequence `n ↦ arⁿ` is `a(1-rⁿ)/(1-r)`
+
+```agda
+sum-standard-geometric-fin-sequence-ℚ : ℚ → ℚ → ℕ → ℚ
+sum-standard-geometric-fin-sequence-ℚ =
+  sum-standard-geometric-fin-sequence-Commutative-Ring commutative-ring-ℚ
+
+module _
+  (a r : ℚ) (r≠1 : r ≠ one-ℚ)
+  where
+
+  abstract
+    compute-sum-standard-geometric-fin-sequence-ℚ :
+      (n : ℕ) →
+      sum-standard-geometric-fin-sequence-ℚ a r n ＝
+      ( a *ℚ
+        ( (one-ℚ -ℚ power-ℚ n r) *ℚ
+          rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
+    compute-sum-standard-geometric-fin-sequence-ℚ 0 =
+      inv
+        ( equational-reasoning
+          a *ℚ ((one-ℚ -ℚ one-ℚ) *ℚ _)
+          ＝ a *ℚ (zero-ℚ *ℚ _)
+            by
+              ap-mul-ℚ
+                ( refl)
+                ( ap-mul-ℚ (right-inverse-law-add-ℚ one-ℚ) refl)
+          ＝ a *ℚ zero-ℚ
+            by ap-mul-ℚ refl (left-zero-law-mul-ℚ _)
+          ＝ zero-ℚ
+            by right-zero-law-mul-ℚ a)
+    compute-sum-standard-geometric-fin-sequence-ℚ (succ-ℕ n) =
+      let
+        1/⟨1-r⟩ = rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
+      in
+        equational-reasoning
+          sum-standard-geometric-fin-sequence-ℚ a r (succ-ℕ n)
+          ＝
+            sum-standard-geometric-fin-sequence-ℚ a r n +ℚ
+            seq-standard-geometric-sequence-ℚ a r n
+            by
+              cons-sum-fin-sequence-type-Commutative-Ring
+                ( commutative-ring-ℚ)
+                ( n)
+                ( _)
+                ( refl)
+          ＝
+            ( a *ℚ
+              ( (one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩)) +ℚ
+            ( a *ℚ power-ℚ n r)
+            by
+              ap-add-ℚ
+                ( compute-sum-standard-geometric-fin-sequence-ℚ n)
+                ( compute-standard-geometric-sequence-ℚ a r n)
+          ＝
+            a *ℚ
+            (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩) +ℚ power-ℚ n r)
+            by inv (left-distributive-mul-add-ℚ a _ _)
+          ＝
+            a *ℚ
+            ( (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩) +ℚ
+              (power-ℚ n r *ℚ (one-ℚ -ℚ r)) *ℚ 1/⟨1-r⟩))
+            by
+              ap-mul-ℚ
+                ( refl)
+                ( ap-add-ℚ
+                  ( refl)
+                  ( inv
+                    ( cancel-right-mul-div-ℚˣ _
+                      ( invertible-diff-neq-ℚ r one-ℚ r≠1))))
+          ＝
+            a *ℚ
+            ( ( (one-ℚ -ℚ power-ℚ n r) +ℚ (power-ℚ n r *ℚ (one-ℚ -ℚ r))) *ℚ
+              1/⟨1-r⟩)
+            by
+              ap-mul-ℚ
+                ( refl)
+                ( inv (right-distributive-mul-add-ℚ _ _ 1/⟨1-r⟩))
+          ＝
+            a *ℚ
+            ( ( one-ℚ -ℚ power-ℚ n r +ℚ
+                ((power-ℚ n r *ℚ one-ℚ) -ℚ (power-ℚ n r *ℚ r))) *ℚ
+              1/⟨1-r⟩)
+            by
+              ap-mul-ℚ
+                ( refl)
+                ( ap-mul-ℚ
+                  ( ap-add-ℚ refl (left-distributive-mul-diff-ℚ _ _ _))
+                  ( refl))
+          ＝
+            a *ℚ
+            ( ( one-ℚ -ℚ power-ℚ n r +ℚ
+                ((power-ℚ n r -ℚ power-ℚ (succ-ℕ n) r))) *ℚ
+              1/⟨1-r⟩)
+            by
+              ap-mul-ℚ
+                ( refl)
+                ( ap-mul-ℚ
+                  ( ap-add-ℚ
+                    ( refl)
+                    ( ap-diff-ℚ
+                      ( right-unit-law-mul-ℚ _)
+                      ( inv (power-succ-ℚ n r))))
+                  ( refl))
+          ＝ a *ℚ ((one-ℚ -ℚ power-ℚ (succ-ℕ n) r) *ℚ 1/⟨1-r⟩)
+            by
+              ap-mul-ℚ
+                ( refl)
+                ( ap-mul-ℚ
+                  ( mul-right-div-Group group-add-ℚ _ _ _)
+                  ( refl))
+```
+
+## External links
+
+- [Geometric progressions](https://en.wikipedia.org/wiki/Geometric_progression)
+  at Wikipedia
diff --git a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md
index 5d298f8985..1345443d5b 100644
--- a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md
@@ -9,6 +9,8 @@ module elementary-number-theory.multiplicative-group-of-rational-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.multiplication-positive-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
@@ -26,6 +28,7 @@ open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.negated-equality
 open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
@@ -86,6 +89,9 @@ _*ℚˣ_ = mul-ℚˣ
 
 inv-ℚˣ : ℚˣ → ℚˣ
 inv-ℚˣ = inv-group-of-units-Ring ring-ℚ
+
+rational-inv-ℚˣ : ℚˣ → ℚ
+rational-inv-ℚˣ q = rational-ℚˣ (inv-ℚˣ q)
 ```
 
 ### Inverse laws in the multiplicative group of rational numbers
@@ -169,3 +175,35 @@ invertible-ℚ⁺ = invertible-nonzero-ℚ ∘ nonzero-ℚ⁺
 invertible-ℚ⁻ : ℚ⁻ → ℚˣ
 invertible-ℚ⁻ = invertible-nonzero-ℚ ∘ nonzero-ℚ⁻
 ```
+
+### If `a ≠ b`, `b - a` is invertible
+
+```agda
+abstract
+  is-invertible-diff-neq-ℚ :
+    (a b : ℚ) → a ≠ b → is-invertible-element-Ring ring-ℚ (b -ℚ a)
+  is-invertible-diff-neq-ℚ a b a≠b =
+    is-invertible-element-ring-is-nonzero-ℚ
+      ( b -ℚ a)
+      ( λ b-a=0 → a≠b (inv (eq-is-unit-right-div-Group group-add-ℚ b-a=0)))
+
+invertible-diff-neq-ℚ : (a b : ℚ) → a ≠ b → ℚˣ
+invertible-diff-neq-ℚ a b a≠b = (b -ℚ a , is-invertible-diff-neq-ℚ a b a≠b)
+```
+
+### Cancellation laws
+
+```agda
+abstract
+  cancel-right-mul-div-ℚˣ :
+    (p : ℚ) (q : ℚˣ) → (p *ℚ rational-ℚˣ q) *ℚ rational-inv-ℚˣ q ＝ p
+  cancel-right-mul-div-ℚˣ p q =
+    equational-reasoning
+      p *ℚ rational-ℚˣ q *ℚ rational-inv-ℚˣ q
+      ＝ p *ℚ (rational-ℚˣ q *ℚ rational-inv-ℚˣ q)
+        by associative-mul-ℚ _ _ _
+      ＝ p *ℚ rational-ℚˣ one-ℚˣ
+        by ap-mul-ℚ refl (ap rational-ℚˣ (right-inverse-law-mul-ℚˣ q))
+      ＝ p
+        by right-unit-law-mul-ℚ p
+```
diff --git a/src/group-theory/arithmetic-sequences-semigroups.lagda.md b/src/group-theory/arithmetic-sequences-semigroups.lagda.md
index f58aa8571c..0238c5bd31 100644
--- a/src/group-theory/arithmetic-sequences-semigroups.lagda.md
+++ b/src/group-theory/arithmetic-sequences-semigroups.lagda.md
@@ -13,6 +13,7 @@ open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
@@ -188,6 +189,32 @@ module _
       ( refl)
 ```
 
+### The tail of a standard arithmetic sequence is another standard arithmetic sequence
+
+```agda
+module _
+  {l : Level} (G : Semigroup l) (a d : type-Semigroup G)
+  where
+
+  abstract
+    htpy-tail-standard-arithmetric-sequence-Semigroup :
+      tail-sequence
+        ( seq-standard-arithmetic-sequence-Semigroup G a d) ~
+      seq-standard-arithmetic-sequence-Semigroup G (mul-Semigroup G a d) d
+    htpy-tail-standard-arithmetric-sequence-Semigroup 0 = refl
+    htpy-tail-standard-arithmetric-sequence-Semigroup (succ-ℕ n) =
+      ap-mul-Semigroup G
+        ( htpy-tail-standard-arithmetric-sequence-Semigroup n)
+        ( refl)
+
+    eq-tail-standard-arithmetric-sequence-Semigroup :
+      tail-sequence
+        ( seq-standard-arithmetic-sequence-Semigroup G a d) ＝
+      seq-standard-arithmetic-sequence-Semigroup G (mul-Semigroup G a d) d
+    eq-tail-standard-arithmetric-sequence-Semigroup =
+      eq-htpy htpy-tail-standard-arithmetric-sequence-Semigroup
+```
+
 ## External links
 
 - [Arithmetic progressions](https://en.wikipedia.org/wiki/Arithmetic_progression)
diff --git a/src/lists/sequences.lagda.md b/src/lists/sequences.lagda.md
index 41905ca59a..242bc05b7f 100644
--- a/src/lists/sequences.lagda.md
+++ b/src/lists/sequences.lagda.md
@@ -7,6 +7,8 @@ module lists.sequences where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
@@ -38,6 +40,13 @@ sequence : {l : Level} → UU l → UU l
 sequence A = dependent-sequence (λ _ → A)
 ```
 
+### The tail of a sequence
+
+```agda
+tail-sequence : {l : Level} {A : UU l} → sequence A → sequence A
+tail-sequence u n = u (succ-ℕ n)
+```
+
 ### Functorial action on maps of sequences
 
 ```agda
diff --git a/src/ring-theory.lagda.md b/src/ring-theory.lagda.md
index 945dff35bf..4c54a3e822 100644
--- a/src/ring-theory.lagda.md
+++ b/src/ring-theory.lagda.md
@@ -32,6 +32,7 @@ open import ring-theory.full-ideals-rings public
 open import ring-theory.function-rings public
 open import ring-theory.function-semirings public
 open import ring-theory.generating-elements-rings public
+open import ring-theory.geometric-sequences-rings public
 open import ring-theory.geometric-sequences-semirings public
 open import ring-theory.groups-of-units-rings public
 open import ring-theory.homomorphisms-cyclic-rings public
diff --git a/src/ring-theory/geometric-sequences-rings.lagda.md b/src/ring-theory/geometric-sequences-rings.lagda.md
new file mode 100644
index 0000000000..2d415a0512
--- /dev/null
+++ b/src/ring-theory/geometric-sequences-rings.lagda.md
@@ -0,0 +1,215 @@
+# Geometric sequences in rings
+
+```agda
+module ring-theory.geometric-sequences-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.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.arithmetic-sequences-semigroups
+
+open import lists.sequences
+
+open import ring-theory.geometric-sequences-semirings
+open import ring-theory.powers-of-elements-rings
+open import ring-theory.rings
+```
+
+</details>
+
+## Ideas
+
+A
+{{#concept "geometric sequence" Disambiguation="in a ring" Agda=geometric-sequence-Ring}}
+in a [ring](ring-theory.rings.md) is a
+[geometric sequence](ring-theory.geometric-sequences-semirings.md) in the
+underlying [semiring](ring-theory.semirings.md).
+
+These are sequences of the form `n ↦ a * rⁿ`, for elements `a`, `r` in the ring.
+
+## Definitions
+
+### Geometric sequences in rings
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  geometric-sequence-Ring : UU l
+  geometric-sequence-Ring =
+    geometric-sequence-Semiring (semiring-Ring R)
+
+module _
+  {l : Level} (R : Ring l)
+  (u : geometric-sequence-Ring R)
+  where
+
+  seq-geometric-sequence-Ring : ℕ → type-Ring R
+  seq-geometric-sequence-Ring =
+    seq-geometric-sequence-Semiring (semiring-Ring R) u
+
+  common-ratio-geometric-sequence-Ring : type-Ring R
+  common-ratio-geometric-sequence-Ring =
+    common-ratio-geometric-sequence-Semiring (semiring-Ring R) u
+
+  is-common-ratio-geometric-sequence-Ring :
+    ( n : ℕ) →
+    ( seq-geometric-sequence-Ring (succ-ℕ n)) ＝
+    ( mul-Ring
+      ( R)
+      ( seq-geometric-sequence-Ring n)
+      ( common-ratio-geometric-sequence-Ring))
+  is-common-ratio-geometric-sequence-Ring =
+    is-common-difference-arithmetic-sequence-Semigroup
+      ( multiplicative-semigroup-Ring R)
+      ( u)
+
+  initial-term-geometric-sequence-Ring : type-Ring R
+  initial-term-geometric-sequence-Ring =
+    initial-term-arithmetic-sequence-Semigroup
+      ( multiplicative-semigroup-Ring R)
+      ( u)
+```
+
+### The standard geometric sequences in a ring
+
+The standard geometric sequence with initial term `a` and common factor `r` is
+the sequence `u` defined by:
+
+- `u₀ = a`
+- `uₙ₊₁ = uₙ * r`
+
+```agda
+module _
+  {l : Level} (R : Ring l) (a r : type-Ring R)
+  where
+
+  standard-geometric-sequence-Ring : geometric-sequence-Ring R
+  standard-geometric-sequence-Ring =
+    standard-arithmetic-sequence-Semigroup
+      ( multiplicative-semigroup-Ring R)
+      ( a)
+      ( r)
+
+  seq-standard-geometric-sequence-Ring : ℕ → type-Ring R
+  seq-standard-geometric-sequence-Ring =
+    seq-geometric-sequence-Ring R
+      standard-geometric-sequence-Ring
+```
+
+### The geometric sequences `n ↦ a * rⁿ`
+
+```agda
+module _
+  {l : Level} (R : Ring l) (a r : type-Ring R)
+  where
+
+  mul-pow-nat-Ring : sequence (type-Ring R)
+  mul-pow-nat-Ring = mul-pow-nat-Semiring (semiring-Ring R) a r
+
+  geometric-mul-pow-nat-Ring : geometric-sequence-Ring R
+  geometric-mul-pow-nat-Ring =
+    geometric-mul-pow-nat-Semiring (semiring-Ring R) a r
+
+  initial-term-mul-pow-nat-Ring : type-Ring R
+  initial-term-mul-pow-nat-Ring =
+    initial-term-mul-pow-nat-Semiring (semiring-Ring R) a r
+
+  eq-initial-term-mul-pow-nat-Ring :
+    initial-term-mul-pow-nat-Ring ＝ a
+  eq-initial-term-mul-pow-nat-Ring =
+    eq-initial-term-mul-pow-nat-Semiring (semiring-Ring R) a r
+```
+
+## Properties
+
+### Any geometric sequence is homotopic to a standard geometric sequence
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  (u : geometric-sequence-Ring R)
+  where
+
+  htpy-seq-standard-geometric-sequence-Ring :
+    ( seq-geometric-sequence-Ring R
+      ( standard-geometric-sequence-Ring R
+        ( initial-term-geometric-sequence-Ring R u)
+        ( common-ratio-geometric-sequence-Ring R u))) ~
+    ( seq-geometric-sequence-Ring R u)
+  htpy-seq-standard-geometric-sequence-Ring =
+    htpy-seq-standard-arithmetic-sequence-Semigroup
+      ( multiplicative-semigroup-Ring R)
+      ( u)
+```
+
+### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
+
+```agda
+module _
+  {l : Level} (R : Ring l) (a r : type-Ring R)
+  where
+
+  htpy-mul-pow-standard-geometric-sequence-Ring :
+    mul-pow-nat-Ring R a r ~ seq-standard-geometric-sequence-Ring R a r
+  htpy-mul-pow-standard-geometric-sequence-Ring =
+    htpy-mul-pow-standard-geometric-sequence-Semiring (semiring-Ring R) a r
+```
+
+```agda
+module _
+  {l : Level} (R : Ring l) (u : geometric-sequence-Ring R)
+  where
+
+  htpy-mul-pow-geometric-sequence-Ring :
+    mul-pow-nat-Ring
+      ( R)
+      ( initial-term-geometric-sequence-Ring R u)
+      ( common-ratio-geometric-sequence-Ring R u) ~
+    seq-geometric-sequence-Ring R u
+  htpy-mul-pow-geometric-sequence-Ring =
+    htpy-mul-pow-geometric-sequence-Semiring (semiring-Ring R) u
+```
+
+### Constant sequences are geometric with common ratio one
+
+```agda
+module _
+  {l : Level} (R : Ring l) (a : type-Ring R)
+  where
+
+  one-is-common-ratio-const-sequence-Ring :
+    is-common-difference-sequence-Semigroup
+      ( multiplicative-semigroup-Ring R)
+      ( λ _ → a)
+      ( one-Ring R)
+  one-is-common-ratio-const-sequence-Ring n =
+    inv (right-unit-law-mul-Ring R a)
+
+  geometric-const-sequence-Ring : geometric-sequence-Ring R
+  geometric-const-sequence-Ring =
+    geometric-const-sequence-Semiring (semiring-Ring R) a
+```
+
+## See also
+
+- [Geometric sequences in a semiring](ring-theory.geometric-sequences-semirings.md)
+
+## External links
+
+- [Geometric progressions](https://en.wikipedia.org/wiki/Geometric_progression)
+  at Wikipedia
diff --git a/src/ring-theory/geometric-sequences-semirings.lagda.md b/src/ring-theory/geometric-sequences-semirings.lagda.md
index 2b0107a2db..1e560ceabd 100644
--- a/src/ring-theory/geometric-sequences-semirings.lagda.md
+++ b/src/ring-theory/geometric-sequences-semirings.lagda.md
@@ -13,6 +13,7 @@ open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
@@ -54,6 +55,11 @@ module _
     arithmetic-sequence-Semigroup
       ( multiplicative-semigroup-Semiring R)
 
+  is-geometric-sequence-Semiring : sequence (type-Semiring R) → UU l
+  is-geometric-sequence-Semiring =
+    is-arithmetic-sequence-Semigroup
+      ( multiplicative-semigroup-Semiring R)
+
 module _
   {l : Level} (R : Semiring l)
   (u : geometric-sequence-Semiring R)
@@ -66,8 +72,8 @@ module _
       ( u)
 
   is-geometric-seq-geometric-sequence-Semiring :
-    is-arithmetic-sequence-Semigroup
-      ( multiplicative-semigroup-Semiring R)
+    is-geometric-sequence-Semiring
+      ( R)
       ( seq-geometric-sequence-Semiring)
   is-geometric-seq-geometric-sequence-Semiring =
     is-arithmetic-seq-arithmetic-sequence-Semigroup
@@ -205,7 +211,7 @@ module _
       ( u)
 ```
 
-### The nth term of an geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
+### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
 
 ```agda
 module _
@@ -267,6 +273,32 @@ module _
     ( one-Semiring R , one-is-common-ratio-const-sequence-Semiring)
 ```
 
+### The tail of a standard geometric sequence is another standard geometric sequence
+
+```agda
+module _
+  {l : Level} (R : Semiring l) (a r : type-Semiring R)
+  where
+
+  abstract
+    htpy-tail-standard-geometric-sequence-Semiring :
+      tail-sequence
+        ( seq-standard-geometric-sequence-Semiring R a r) ~
+      seq-standard-geometric-sequence-Semiring R (mul-Semiring R a r) r
+    htpy-tail-standard-geometric-sequence-Semiring =
+      htpy-tail-standard-arithmetric-sequence-Semigroup
+        ( multiplicative-semigroup-Semiring R)
+        ( a)
+        ( r)
+
+    eq-tail-standard-geometric-sequence-Semiring :
+      tail-sequence
+        ( seq-standard-geometric-sequence-Semiring R a r) ＝
+      seq-standard-geometric-sequence-Semiring R (mul-Semiring R a r) r
+    eq-tail-standard-geometric-sequence-Semiring =
+      eq-htpy htpy-tail-standard-geometric-sequence-Semiring
+```
+
 ## External links
 
 - [Geometric progressions](https://en.wikipedia.org/wiki/Geometric_progression)