diff --git a/src/commutative-algebra/local-commutative-rings.lagda.md b/src/commutative-algebra/local-commutative-rings.lagda.md
index 9de71b60fc..717095eaa5 100644
--- a/src/commutative-algebra/local-commutative-rings.lagda.md
+++ b/src/commutative-algebra/local-commutative-rings.lagda.md
@@ -66,4 +66,24 @@ module _
   is-local-commutative-ring-Local-Commutative-Ring :
     is-local-Commutative-Ring commutative-ring-Local-Commutative-Ring
   is-local-commutative-ring-Local-Commutative-Ring = pr2 A
+
+  zero-Local-Commutative-Ring : type-Local-Commutative-Ring
+  zero-Local-Commutative-Ring = zero-Ring ring-Local-Commutative-Ring
+
+  one-Local-Commutative-Ring : type-Local-Commutative-Ring
+  one-Local-Commutative-Ring = one-Ring ring-Local-Commutative-Ring
+
+  add-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring →
+    type-Local-Commutative-Ring
+  add-Local-Commutative-Ring = add-Ring ring-Local-Commutative-Ring
+
+  mul-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring →
+    type-Local-Commutative-Ring
+  mul-Local-Commutative-Ring = mul-Ring ring-Local-Commutative-Ring
+
+  neg-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring
+  neg-Local-Commutative-Ring = neg-Ring ring-Local-Commutative-Ring
 ```
diff --git a/src/complex-numbers.lagda.md b/src/complex-numbers.lagda.md
index bb5ba406cb..14b808adef 100644
--- a/src/complex-numbers.lagda.md
+++ b/src/complex-numbers.lagda.md
@@ -4,6 +4,7 @@
 module complex-numbers where
 
 open import complex-numbers.addition-complex-numbers public
+open import complex-numbers.addition-nonzero-complex-numbers public
 open import complex-numbers.apartness-complex-numbers public
 open import complex-numbers.complex-numbers public
 open import complex-numbers.conjugation-complex-numbers public
@@ -11,6 +12,7 @@ open import complex-numbers.eisenstein-integers public
 open import complex-numbers.gaussian-integers public
 open import complex-numbers.large-additive-group-of-complex-numbers public
 open import complex-numbers.large-ring-of-complex-numbers public
+open import complex-numbers.local-ring-of-complex-numbers public
 open import complex-numbers.magnitude-complex-numbers public
 open import complex-numbers.multiplication-complex-numbers public
 open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers public
diff --git a/src/complex-numbers/addition-nonzero-complex-numbers.lagda.md b/src/complex-numbers/addition-nonzero-complex-numbers.lagda.md
new file mode 100644
index 0000000000..c74857b7bf
--- /dev/null
+++ b/src/complex-numbers/addition-nonzero-complex-numbers.lagda.md
@@ -0,0 +1,53 @@
+# Addition of nonzero complex numbers
+
+```agda
+module complex-numbers.addition-nonzero-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import complex-numbers.addition-complex-numbers
+open import complex-numbers.complex-numbers
+open import complex-numbers.nonzero-complex-numbers
+
+open import foundation.disjunction
+open import foundation.functoriality-disjunction
+open import foundation.universe-levels
+
+open import real-numbers.addition-nonzero-real-numbers
+open import real-numbers.nonzero-real-numbers
+```
+
+</details>
+
+## Idea
+
+This file describes properties of
+[addition](complex-numbers.addition-complex-numbers.md) of
+[nonzero](complex-numbers.nonzero-complex-numbers.md)
+[complex numbers](complex-numbers.complex-numbers.md).
+
+## Properties
+
+### If the sum of two complex numbers is nonzero, one of them is nonzero
+
+```agda
+abstract
+  is-nonzero-either-is-nonzero-add-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → is-nonzero-ℂ (z +ℂ w) →
+    disjunction-type (is-nonzero-ℂ z) (is-nonzero-ℂ w)
+  is-nonzero-either-is-nonzero-add-ℂ z@(a +iℂ b) w@(c +iℂ d) =
+    elim-disjunction
+      ( is-nonzero-prop-ℂ z ∨ is-nonzero-prop-ℂ w)
+      ( λ a+c≠0 →
+        map-disjunction
+          ( inl-disjunction)
+          ( inl-disjunction)
+          ( is-nonzero-either-is-nonzero-add-ℝ a c a+c≠0))
+      ( λ b+d≠0 →
+        map-disjunction
+          ( inr-disjunction)
+          ( inr-disjunction)
+          ( is-nonzero-either-is-nonzero-add-ℝ b d b+d≠0))
+```
diff --git a/src/complex-numbers/local-ring-of-complex-numbers.lagda.md b/src/complex-numbers/local-ring-of-complex-numbers.lagda.md
new file mode 100644
index 0000000000..6f96731b10
--- /dev/null
+++ b/src/complex-numbers/local-ring-of-complex-numbers.lagda.md
@@ -0,0 +1,50 @@
+# The local ring of complex numbers
+
+```agda
+module complex-numbers.local-ring-of-complex-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.local-commutative-rings
+
+open import complex-numbers.addition-complex-numbers
+open import complex-numbers.addition-nonzero-complex-numbers
+open import complex-numbers.large-ring-of-complex-numbers
+open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers
+open import complex-numbers.nonzero-complex-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.functoriality-disjunction
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The
+[commutative ring of complex numbers](complex-numbers.large-ring-of-complex-numbers.md)
+is [local](commutative-algebra.local-commutative-rings.md).
+
+## Definition
+
+```agda
+is-local-commutative-ring-ℂ :
+  (l : Level) → is-local-Commutative-Ring (commutative-ring-ℂ l)
+is-local-commutative-ring-ℂ l z w is-invertible-z+w =
+  map-disjunction
+    ( is-invertible-is-nonzero-ℂ z)
+    ( is-invertible-is-nonzero-ℂ w)
+    ( is-nonzero-either-is-nonzero-add-ℂ
+      ( z)
+      ( w)
+      ( is-nonzero-is-invertible-ℂ
+        ( z +ℂ w)
+        ( is-invertible-z+w)))
+
+local-commutative-ring-ℂ : (l : Level) → Local-Commutative-Ring (lsuc l)
+local-commutative-ring-ℂ l =
+  ( commutative-ring-ℂ l , is-local-commutative-ring-ℂ l)
+```
diff --git a/src/complex-numbers/magnitude-complex-numbers.lagda.md b/src/complex-numbers/magnitude-complex-numbers.lagda.md
index f151528dc4..3c033afa8d 100644
--- a/src/complex-numbers/magnitude-complex-numbers.lagda.md
+++ b/src/complex-numbers/magnitude-complex-numbers.lagda.md
@@ -12,11 +12,14 @@ module complex-numbers.magnitude-complex-numbers where
 open import complex-numbers.complex-numbers
 open import complex-numbers.conjugation-complex-numbers
 open import complex-numbers.multiplication-complex-numbers
+open import complex-numbers.similarity-complex-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
+open import real-numbers.absolute-value-real-numbers
 open import real-numbers.addition-nonnegative-real-numbers
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
@@ -25,6 +28,7 @@ open import real-numbers.multiplication-nonnegative-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.negation-real-numbers
 open import real-numbers.nonnegative-real-numbers
+open import real-numbers.positive-real-numbers
 open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
@@ -225,3 +229,67 @@ abstract
       ＝ magnitude-ℂ z *ℝ magnitude-ℂ w
         by ap real-ℝ⁰⁺ (distributive-sqrt-mul-ℝ⁰⁺ _ _)
 ```
+
+### The magnitude of a real number as a complex number is its absolute value
+
+```agda
+abstract
+  magnitude-complex-ℝ :
+    {l : Level} (x : ℝ l) → magnitude-ℂ (complex-ℝ x) ＝ abs-ℝ x
+  magnitude-complex-ℝ {l} x =
+    equational-reasoning
+      real-sqrt-ℝ⁰⁺
+        ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ (raise-ℝ l zero-ℝ))
+      ＝
+        real-sqrt-ℝ⁰⁺
+          ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ zero-ℝ)
+        by
+          ap
+            ( real-sqrt-ℝ⁰⁺)
+            ( eq-ℝ⁰⁺ _ _
+              ( eq-sim-ℝ
+                ( preserves-sim-left-add-ℝ _ _ _
+                  ( preserves-sim-square-ℝ
+                    ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))))))
+      ＝ real-sqrt-ℝ⁰⁺ (nonnegative-square-ℝ x +ℝ⁰⁺ zero-ℝ⁰⁺)
+        by ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (ap-add-ℝ refl square-zero-ℝ))
+      ＝ real-sqrt-ℝ⁰⁺ (nonnegative-square-ℝ x)
+        by ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (right-unit-law-add-ℝ _))
+      ＝ abs-ℝ x
+        by inv (eq-abs-sqrt-square-ℝ x)
+```
+
+### Similar complex numbers have similar magnitudes
+
+```agda
+abstract
+  preserves-sim-squared-magnitude-ℂ :
+    {l1 l2 : Level} {z : ℂ l1} {w : ℂ l2} →
+    sim-ℂ z w → sim-ℝ (squared-magnitude-ℂ z) (squared-magnitude-ℂ w)
+  preserves-sim-squared-magnitude-ℂ (a~c , b~d) =
+    preserves-sim-add-ℝ
+      ( preserves-sim-square-ℝ a~c)
+      ( preserves-sim-square-ℝ b~d)
+
+  preserves-sim-magnitude-ℂ :
+    {l1 l2 : Level} {z : ℂ l1} {w : ℂ l2} →
+    sim-ℂ z w → sim-ℝ (magnitude-ℂ z) (magnitude-ℂ w)
+  preserves-sim-magnitude-ℂ z~w =
+    preserves-sim-sqrt-ℝ⁰⁺ _ _ (preserves-sim-squared-magnitude-ℂ z~w)
+```
+
+### The magnitude of `one-ℂ` is `one-ℝ`
+
+```agda
+abstract
+  magnitude-one-ℂ : magnitude-ℂ one-ℂ ＝ one-ℝ
+  magnitude-one-ℂ =
+    equational-reasoning
+      magnitude-ℂ one-ℂ
+      ＝ magnitude-ℂ (complex-ℝ one-ℝ)
+        by ap magnitude-ℂ (inv eq-complex-one-ℝ)
+      ＝ abs-ℝ one-ℝ
+        by magnitude-complex-ℝ one-ℝ
+      ＝ one-ℝ
+        by abs-real-ℝ⁺ one-ℝ⁺
+```
diff --git a/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md b/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md
index 183fbec3b2..4d7c38d896 100644
--- a/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md
+++ b/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md
@@ -7,21 +7,34 @@ module complex-numbers.multiplicative-inverses-nonzero-complex-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import commutative-algebra.invertible-elements-commutative-rings
+
 open import complex-numbers.complex-numbers
 open import complex-numbers.conjugation-complex-numbers
+open import complex-numbers.large-ring-of-complex-numbers
 open import complex-numbers.magnitude-complex-numbers
 open import complex-numbers.multiplication-complex-numbers
 open import complex-numbers.nonzero-complex-numbers
+open import complex-numbers.raising-universe-levels-complex-numbers
 open import complex-numbers.similarity-complex-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import real-numbers.multiplication-nonzero-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.multiplicative-inverses-positive-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.nonzero-real-numbers
+open import real-numbers.positive-and-negative-real-numbers
+open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 ```
 
 </details>
@@ -86,3 +99,99 @@ abstract
       ( commutative-mul-ℂ _ _)
       ( right-inverse-law-mul-nonzero-ℂ z)
 ```
+
+### If a complex number has a multiplicative inverse, it is nonzero
+
+```agda
+abstract
+  is-nonzero-has-right-inverse-mul-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → sim-ℂ (z *ℂ w) one-ℂ →
+    is-nonzero-ℂ z
+  is-nonzero-has-right-inverse-mul-ℂ z w zw=1 =
+    is-nonzero-is-positive-magnitude-ℂ
+      ( z)
+      ( elim-disjunction
+        ( is-positive-prop-ℝ (magnitude-ℂ z))
+        ( λ |z|<0 →
+          ex-falso
+            ( is-not-negative-and-nonnegative-ℝ
+              ( |z|<0 , is-nonnegative-real-ℝ⁰⁺ (nonnegative-magnitude-ℂ z))))
+        ( id)
+        ( pr1
+          ( is-nonzero-factors-is-nonzero-mul-ℝ
+            ( (magnitude-ℂ z))
+            ( (magnitude-ℂ w))
+            ( is-nonzero-sim-ℝ
+              ( symmetric-sim-ℝ
+                ( similarity-reasoning-ℝ
+                  (magnitude-ℂ z) *ℝ (magnitude-ℂ w)
+                  ~ℝ magnitude-ℂ (z *ℂ w)
+                    by sim-eq-ℝ (inv (distributive-magnitude-mul-ℂ z w))
+                  ~ℝ magnitude-ℂ one-ℂ
+                    by preserves-sim-magnitude-ℂ zw=1
+                  ~ℝ one-ℝ
+                    by sim-eq-ℝ magnitude-one-ℂ))
+              ( is-nonzero-is-positive-ℝ is-positive-one-ℝ)))))
+
+  is-nonzero-has-left-inverse-mul-ℂ :
+    {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → sim-ℂ (z *ℂ w) one-ℂ →
+    is-nonzero-ℂ w
+  is-nonzero-has-left-inverse-mul-ℂ z w zw=1 =
+    is-nonzero-has-right-inverse-mul-ℂ
+      ( w)
+      ( z)
+      ( tr (λ x → sim-ℂ x one-ℂ) (commutative-mul-ℂ z w) zw=1)
+```
+
+### The multiplicative inverse of a nonzero complex number is nonzero
+
+```agda
+abstract
+  is-nonzero-complex-inv-nonzero-ℂ :
+    {l : Level} (z : nonzero-ℂ l) → is-nonzero-ℂ (complex-inv-nonzero-ℂ z)
+  is-nonzero-complex-inv-nonzero-ℂ z =
+    is-nonzero-has-left-inverse-mul-ℂ
+      ( _)
+      ( _)
+      ( right-inverse-law-mul-nonzero-ℂ z)
+
+inv-nonzero-ℂ : {l : Level} → nonzero-ℂ l → nonzero-ℂ l
+inv-nonzero-ℂ z = (complex-inv-nonzero-ℂ z , is-nonzero-complex-inv-nonzero-ℂ z)
+```
+
+### A complex number is invertible if and only if it is nonzero
+
+```agda
+abstract
+  is-nonzero-is-invertible-ℂ :
+    {l : Level} (z : ℂ l) →
+    is-invertible-element-Commutative-Ring (commutative-ring-ℂ l) z →
+    is-nonzero-ℂ z
+  is-nonzero-is-invertible-ℂ z (w , zw=1 , _) =
+    is-nonzero-has-right-inverse-mul-ℂ
+      ( z)
+      ( w)
+      ( transitive-sim-ℂ _ _ _
+        ( symmetric-sim-ℂ (sim-raise-ℂ _ one-ℂ))
+        ( sim-eq-ℂ zw=1))
+
+  is-invertible-is-nonzero-ℂ :
+    {l : Level} (z : ℂ l) → is-nonzero-ℂ z →
+    is-invertible-element-Commutative-Ring (commutative-ring-ℂ l) z
+  is-invertible-is-nonzero-ℂ z z≠0 =
+    ( complex-inv-nonzero-ℂ (z , z≠0) ,
+      eq-sim-ℂ
+        ( similarity-reasoning-ℂ
+          z *ℂ complex-inv-nonzero-ℂ (z , z≠0)
+          ~ℂ one-ℂ
+            by right-inverse-law-mul-nonzero-ℂ (z , z≠0)
+          ~ℂ raise-ℂ _ one-ℂ
+            by sim-raise-ℂ _ one-ℂ) ,
+      eq-sim-ℂ
+        ( similarity-reasoning-ℂ
+          complex-inv-nonzero-ℂ (z , z≠0) *ℂ z
+          ~ℂ one-ℂ
+            by left-inverse-law-mul-nonzero-ℂ (z , z≠0)
+          ~ℂ raise-ℂ _ one-ℂ
+            by sim-raise-ℂ _ one-ℂ))
+```
diff --git a/src/complex-numbers/nonzero-complex-numbers.lagda.md b/src/complex-numbers/nonzero-complex-numbers.lagda.md
index 9f978a56f1..144fd3127f 100644
--- a/src/complex-numbers/nonzero-complex-numbers.lagda.md
+++ b/src/complex-numbers/nonzero-complex-numbers.lagda.md
@@ -26,6 +26,7 @@ open import real-numbers.positive-and-negative-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
+open import real-numbers.square-roots-nonnegative-real-numbers
 open import real-numbers.squares-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
@@ -99,3 +100,24 @@ positive-squared-magnitude-nonzero-ℂ :
 positive-squared-magnitude-nonzero-ℂ (z , z≠0) =
   ( squared-magnitude-ℂ z , is-positive-squared-magnitude-is-nonzero-ℂ z z≠0)
 ```
+
+### A complex number is nonzero if and only if its magnitude is positive
+
+```agda
+abstract
+  is-nonzero-is-positive-magnitude-ℂ :
+    {l : Level} (z : ℂ l) → is-positive-ℝ (magnitude-ℂ z) → is-nonzero-ℂ z
+  is-nonzero-is-positive-magnitude-ℂ z 0<|z| =
+    is-nonzero-is-positive-squared-magnitude-ℂ
+      ( z)
+      ( is-positive-is-positive-sqrt-ℝ⁰⁺
+        ( nonnegative-squared-magnitude-ℂ z)
+        ( 0<|z|))
+
+  is-positive-magnitude-is-nonzero-ℂ :
+    {l : Level} (z : ℂ l) → is-nonzero-ℂ z → is-positive-ℝ (magnitude-ℂ z)
+  is-positive-magnitude-is-nonzero-ℂ z z≠0 =
+    is-positive-sqrt-is-positive-ℝ⁰⁺
+      ( nonnegative-squared-magnitude-ℂ z)
+      ( is-positive-squared-magnitude-is-nonzero-ℂ z z≠0)
+```
diff --git a/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
index 698a8adb82..3c44fa5f0c 100644
--- a/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
@@ -26,6 +26,7 @@ open import elementary-number-theory.minima-and-maxima-rational-numbers
 open import elementary-number-theory.minimum-rational-numbers
 open import elementary-number-theory.multiplication-negative-rational-numbers
 open import elementary-number-theory.multiplication-nonnegative-rational-numbers
+open import elementary-number-theory.multiplication-positive-and-negative-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-group-of-positive-rational-numbers
@@ -46,12 +47,14 @@ open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.cartesian-product-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.empty-types
 open import foundation.existential-quantification
 open import foundation.function-extensionality
 open import foundation.function-types
+open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.images-subtypes
 open import foundation.logical-equivalences
@@ -1287,3 +1290,79 @@ abstract
               ( neg-ℚ⁰⁺ (nonnegative-square-ℚ q))
               ( nonnegative-square-ℚ q))
 ```
+
+### If the lower bound of the product of `[a, b]` and `[c, d]` is positive, then `a`, `b`, `c`, and `d` are all positive or all negative
+
+```agda
+abstract
+  same-sign-bounds-is-positive-lower-bound-mul-closed-interval-ℚ :
+    ([a,b] [c,d] : closed-interval-ℚ) →
+    is-positive-ℚ (lower-bound-mul-closed-interval-ℚ [a,b] [c,d]) →
+    ( ( is-negative-ℚ (lower-bound-closed-interval-ℚ [a,b]) ×
+        is-negative-ℚ (upper-bound-closed-interval-ℚ [a,b]) ×
+        is-negative-ℚ (lower-bound-closed-interval-ℚ [c,d]) ×
+        is-negative-ℚ (upper-bound-closed-interval-ℚ [c,d])) +
+      ( is-positive-ℚ (lower-bound-closed-interval-ℚ [a,b]) ×
+        is-positive-ℚ (upper-bound-closed-interval-ℚ [a,b]) ×
+        is-positive-ℚ (lower-bound-closed-interval-ℚ [c,d]) ×
+        is-positive-ℚ (upper-bound-closed-interval-ℚ [c,d])))
+  same-sign-bounds-is-positive-lower-bound-mul-closed-interval-ℚ
+    [a,b]@((a , b) , _) [c,d]@((c , d) , _) is-pos-lb =
+    let
+      same-sign-a-c =
+        same-sign-is-positive-mul-ℚ
+          ( is-positive-leq-ℚ⁺
+            ( _ , is-pos-lb)
+            ( transitive-leq-ℚ _ _ _ (leq-left-min-ℚ _ _) (leq-left-min-ℚ _ _)))
+      same-sign-a-d =
+        same-sign-is-positive-mul-ℚ
+          ( is-positive-leq-ℚ⁺
+            ( _ , is-pos-lb)
+            ( transitive-leq-ℚ _ _ _
+              ( leq-right-min-ℚ _ _)
+              ( leq-left-min-ℚ _ _)))
+      same-sign-b-d =
+        same-sign-is-positive-mul-ℚ
+          ( is-positive-leq-ℚ⁺
+            ( _ , is-pos-lb)
+            ( transitive-leq-ℚ _ _ _
+              ( leq-right-min-ℚ _ _)
+              ( leq-right-min-ℚ _ _)))
+    in
+      map-coproduct
+        ( λ (is-neg-a , is-neg-c) →
+          let
+            is-neg-d =
+              rec-coproduct
+                ( pr2)
+                ( λ (is-pos-a , _) →
+                  ex-falso
+                    ( is-not-negative-and-positive-ℚ (is-neg-a , is-pos-a)))
+                ( same-sign-a-d)
+            is-neg-b =
+              rec-coproduct
+                ( pr1)
+                ( λ (_ , is-pos-d) →
+                  ex-falso
+                    ( is-not-negative-and-positive-ℚ (is-neg-d , is-pos-d)))
+                ( same-sign-b-d)
+          in (is-neg-a , is-neg-b , is-neg-c , is-neg-d))
+        ( λ (is-pos-a , is-pos-c) →
+          let
+            is-pos-d =
+              rec-coproduct
+                ( λ (is-neg-a , _) →
+                  ex-falso
+                    ( is-not-negative-and-positive-ℚ (is-neg-a , is-pos-a)))
+                ( pr2)
+                ( same-sign-a-d)
+            is-pos-b =
+              rec-coproduct
+                ( λ (_ , is-neg-d) →
+                  ex-falso
+                    ( is-not-negative-and-positive-ℚ (is-neg-d , is-pos-d)))
+                ( pr1)
+                ( same-sign-b-d)
+          in (is-pos-a , is-pos-b , is-pos-c , is-pos-d))
+        ( same-sign-a-c)
+```
diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md
index 4cbe0a9111..1c3ee2661d 100644
--- a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md
@@ -21,6 +21,7 @@ open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
+open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.transport-along-identifications
 ```
@@ -169,3 +170,32 @@ abstract
             ( y≠0)
             ( λ is-pos-y → inr (is-pos-x , is-pos-y)))
 ```
+
+### If `xy` is negative, one of `x` and `y` is positive and the other negative
+
+```agda
+abstract
+  different-signs-is-negative-mul-ℚ :
+    {x y : ℚ} → is-negative-ℚ (x *ℚ y) →
+    ( ( is-positive-ℚ x × is-negative-ℚ y) +
+      ( is-negative-ℚ x × is-positive-ℚ y))
+  different-signs-is-negative-mul-ℚ {x} {y} is-neg-xy =
+    map-coproduct
+      ( λ (is-neg-neg-x , is-neg-y) →
+        ( tr
+            ( is-positive-ℚ)
+            ( neg-neg-ℚ x)
+            ( is-positive-neg-is-negative-ℚ is-neg-neg-x) ,
+          is-neg-y))
+      ( λ (is-pos-neg-x , is-pos-y) →
+        ( tr
+            ( is-negative-ℚ)
+            ( neg-neg-ℚ x)
+            ( is-negative-neg-is-positive-ℚ is-pos-neg-x) ,
+          is-pos-y))
+      ( same-sign-is-positive-mul-ℚ
+        ( inv-tr
+          ( is-positive-ℚ)
+          ( left-negative-law-mul-ℚ x y)
+          ( is-positive-neg-is-negative-ℚ is-neg-xy)))
+```
diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index ba50e0c42c..474d03f52e 100644
--- a/src/linear-algebra.lagda.md
+++ b/src/linear-algebra.lagda.md
@@ -5,6 +5,7 @@
 ```agda
 module linear-algebra where
 
+open import linear-algebra.complex-vector-spaces public
 open import linear-algebra.constant-matrices public
 open import linear-algebra.constant-tuples public
 open import linear-algebra.dependent-products-left-modules-commutative-rings public
@@ -33,6 +34,7 @@ open import linear-algebra.matrices-on-rings public
 open import linear-algebra.multiplication-matrices public
 open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
 open import linear-algebra.rational-modules public
+open import linear-algebra.real-vector-spaces public
 open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public
 open import linear-algebra.scalar-multiplication-tuples public
@@ -46,4 +48,5 @@ open import linear-algebra.tuples-on-euclidean-domains public
 open import linear-algebra.tuples-on-monoids public
 open import linear-algebra.tuples-on-rings public
 open import linear-algebra.tuples-on-semirings public
+open import linear-algebra.vector-spaces public
 ```
diff --git a/src/linear-algebra/complex-vector-spaces.lagda.md b/src/linear-algebra/complex-vector-spaces.lagda.md
new file mode 100644
index 0000000000..23c97e5303
--- /dev/null
+++ b/src/linear-algebra/complex-vector-spaces.lagda.md
@@ -0,0 +1,144 @@
+# Complex vector spaces
+
+```agda
+module linear-algebra.complex-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import complex-numbers.local-ring-of-complex-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.vector-spaces
+```
+
+</details>
+
+## Idea
+
+```agda
+ℂ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+ℂ-Vector-Space l1 l2 = Vector-Space l2 (local-commutative-ring-ℂ l1)
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level} (V : ℂ-Vector-Space l1 l2)
+  where
+
+  ab-ℂ-Vector-Space : Ab l2
+  ab-ℂ-Vector-Space = ab-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  set-ℂ-Vector-Space : Set l2
+  set-ℂ-Vector-Space = set-Ab ab-ℂ-Vector-Space
+
+  type-ℂ-Vector-Space : UU l2
+  type-ℂ-Vector-Space = type-Ab ab-ℂ-Vector-Space
+
+  add-ℂ-Vector-Space :
+    type-ℂ-Vector-Space → type-ℂ-Vector-Space → type-ℂ-Vector-Space
+  add-ℂ-Vector-Space = add-Ab ab-ℂ-Vector-Space
+
+  zero-ℂ-Vector-Space : type-ℂ-Vector-Space
+  zero-ℂ-Vector-Space = zero-Ab ab-ℂ-Vector-Space
+
+  neg-ℂ-Vector-Space : type-ℂ-Vector-Space → type-ℂ-Vector-Space
+  neg-ℂ-Vector-Space = neg-Ab ab-ℂ-Vector-Space
+
+  mul-ℂ-Vector-Space : ℂ l1 → type-ℂ-Vector-Space → type-ℂ-Vector-Space
+  mul-ℂ-Vector-Space = mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  associative-add-ℂ-Vector-Space :
+    (v w x : type-ℂ-Vector-Space) →
+    add-ℂ-Vector-Space (add-ℂ-Vector-Space v w) x ＝
+    add-ℂ-Vector-Space v (add-ℂ-Vector-Space w x)
+  associative-add-ℂ-Vector-Space = associative-add-Ab ab-ℂ-Vector-Space
+
+  left-unit-law-add-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) → add-ℂ-Vector-Space zero-ℂ-Vector-Space v ＝ v
+  left-unit-law-add-ℂ-Vector-Space = left-unit-law-add-Ab ab-ℂ-Vector-Space
+
+  right-unit-law-add-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) → add-ℂ-Vector-Space v zero-ℂ-Vector-Space ＝ v
+  right-unit-law-add-ℂ-Vector-Space = right-unit-law-add-Ab ab-ℂ-Vector-Space
+
+  left-inverse-law-add-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) →
+    add-ℂ-Vector-Space (neg-ℂ-Vector-Space v) v ＝ zero-ℂ-Vector-Space
+  left-inverse-law-add-ℂ-Vector-Space =
+    left-inverse-law-add-Ab ab-ℂ-Vector-Space
+
+  right-inverse-law-add-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) →
+    add-ℂ-Vector-Space v (neg-ℂ-Vector-Space v) ＝ zero-ℂ-Vector-Space
+  right-inverse-law-add-ℂ-Vector-Space =
+    right-inverse-law-add-Ab ab-ℂ-Vector-Space
+
+  commutative-add-ℂ-Vector-Space :
+    (v w : type-ℂ-Vector-Space) →
+    add-ℂ-Vector-Space v w ＝ add-ℂ-Vector-Space w v
+  commutative-add-ℂ-Vector-Space = commutative-add-Ab ab-ℂ-Vector-Space
+
+  left-unit-law-mul-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space (raise-ℂ l1 one-ℂ) v ＝ v
+  left-unit-law-mul-ℂ-Vector-Space =
+    left-unit-law-mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  left-distributive-mul-add-ℂ-Vector-Space :
+    (r : ℂ l1) (v w : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space r (add-ℂ-Vector-Space v w) ＝
+    add-ℂ-Vector-Space (mul-ℂ-Vector-Space r v) (mul-ℂ-Vector-Space r w)
+  left-distributive-mul-add-ℂ-Vector-Space =
+    left-distributive-mul-add-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  right-distributive-mul-add-ℂ-Vector-Space :
+    (r s : ℂ l1) (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space (r +ℂ s) v ＝
+    add-ℂ-Vector-Space (mul-ℂ-Vector-Space r v) (mul-ℂ-Vector-Space s v)
+  right-distributive-mul-add-ℂ-Vector-Space =
+    right-distributive-mul-add-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  associative-mul-ℂ-Vector-Space :
+    (r s : ℂ l1) (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space (r *ℂ s) v ＝
+    mul-ℂ-Vector-Space r (mul-ℂ-Vector-Space s v)
+  associative-mul-ℂ-Vector-Space =
+    associative-mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  left-zero-law-mul-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space (raise-ℂ l1 zero-ℂ) v ＝ zero-ℂ-Vector-Space
+  left-zero-law-mul-ℂ-Vector-Space =
+    left-zero-law-mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  right-zero-law-mul-ℂ-Vector-Space :
+    (r : ℂ l1) →
+    mul-ℂ-Vector-Space r zero-ℂ-Vector-Space ＝ zero-ℂ-Vector-Space
+  right-zero-law-mul-ℂ-Vector-Space =
+    right-zero-law-mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  left-negative-law-mul-ℂ-Vector-Space :
+    (r : ℂ l1) (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space (neg-ℂ r) v ＝
+    neg-ℂ-Vector-Space (mul-ℂ-Vector-Space r v)
+  left-negative-law-mul-ℂ-Vector-Space =
+    left-negative-law-mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  right-negative-law-mul-ℂ-Vector-Space :
+    (r : ℂ l1) (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space r (neg-ℂ-Vector-Space v) ＝
+    neg-ℂ-Vector-Space (mul-ℂ-Vector-Space r v)
+  right-negative-law-mul-ℂ-Vector-Space =
+    right-negative-law-mul-Vector-Space (local-commutative-ring-ℂ l1) V
+
+  mul-neg-one-ℂ-Vector-Space :
+    (v : type-ℂ-Vector-Space) →
+    mul-ℂ-Vector-Space (neg-ℂ (raise-ℂ l1 one-ℂ)) v ＝ neg-ℂ-Vector-Space v
+  mul-neg-one-ℂ-Vector-Space =
+    mul-neg-one-Vector-Space (local-commutative-ring-ℂ l1) V
+```
diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..21ac77abb4
--- /dev/null
+++ b/src/linear-algebra/real-vector-spaces.lagda.md
@@ -0,0 +1,174 @@
+# Real vector spaces
+
+```agda
+module linear-algebra.real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.vector-spaces
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.local-ring-of-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "real vector space" WD="real vector space" WDID=Q46996054 Agda=ℝ-Vector-Space}}
+is a [vector space](linear-algebra.vector-spaces.md) over the
+[local commutative ring of real numbers](real-numbers.local-ring-of-real-numbers.md).
+
+## Definition
+
+```agda
+ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+ℝ-Vector-Space l1 l2 = Vector-Space l2 (local-commutative-ring-ℝ l1)
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2)
+  where
+
+  ab-ℝ-Vector-Space : Ab l2
+  ab-ℝ-Vector-Space = ab-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  set-ℝ-Vector-Space : Set l2
+  set-ℝ-Vector-Space = set-Ab ab-ℝ-Vector-Space
+
+  type-ℝ-Vector-Space : UU l2
+  type-ℝ-Vector-Space = type-Ab ab-ℝ-Vector-Space
+
+  add-ℝ-Vector-Space :
+    type-ℝ-Vector-Space → type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  add-ℝ-Vector-Space = add-Ab ab-ℝ-Vector-Space
+
+  zero-ℝ-Vector-Space : type-ℝ-Vector-Space
+  zero-ℝ-Vector-Space = zero-Ab ab-ℝ-Vector-Space
+
+  neg-ℝ-Vector-Space : type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  neg-ℝ-Vector-Space = neg-Ab ab-ℝ-Vector-Space
+
+  mul-ℝ-Vector-Space : ℝ l1 → type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  mul-ℝ-Vector-Space = mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  associative-add-ℝ-Vector-Space :
+    (v w x : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space (add-ℝ-Vector-Space v w) x ＝
+    add-ℝ-Vector-Space v (add-ℝ-Vector-Space w x)
+  associative-add-ℝ-Vector-Space = associative-add-Ab ab-ℝ-Vector-Space
+
+  left-unit-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) → add-ℝ-Vector-Space zero-ℝ-Vector-Space v ＝ v
+  left-unit-law-add-ℝ-Vector-Space = left-unit-law-add-Ab ab-ℝ-Vector-Space
+
+  right-unit-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) → add-ℝ-Vector-Space v zero-ℝ-Vector-Space ＝ v
+  right-unit-law-add-ℝ-Vector-Space = right-unit-law-add-Ab ab-ℝ-Vector-Space
+
+  left-inverse-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space (neg-ℝ-Vector-Space v) v ＝ zero-ℝ-Vector-Space
+  left-inverse-law-add-ℝ-Vector-Space =
+    left-inverse-law-add-Ab ab-ℝ-Vector-Space
+
+  right-inverse-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space v (neg-ℝ-Vector-Space v) ＝ zero-ℝ-Vector-Space
+  right-inverse-law-add-ℝ-Vector-Space =
+    right-inverse-law-add-Ab ab-ℝ-Vector-Space
+
+  commutative-add-ℝ-Vector-Space :
+    (v w : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space v w ＝ add-ℝ-Vector-Space w v
+  commutative-add-ℝ-Vector-Space = commutative-add-Ab ab-ℝ-Vector-Space
+
+  left-unit-law-mul-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (raise-ℝ l1 one-ℝ) v ＝ v
+  left-unit-law-mul-ℝ-Vector-Space =
+    left-unit-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  left-distributive-mul-add-ℝ-Vector-Space :
+    (r : ℝ l1) (v w : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space r (add-ℝ-Vector-Space v w) ＝
+    add-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space r w)
+  left-distributive-mul-add-ℝ-Vector-Space =
+    left-distributive-mul-add-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  right-distributive-mul-add-ℝ-Vector-Space :
+    (r s : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (r +ℝ s) v ＝
+    add-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space s v)
+  right-distributive-mul-add-ℝ-Vector-Space =
+    right-distributive-mul-add-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  associative-mul-ℝ-Vector-Space :
+    (r s : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (r *ℝ s) v ＝
+    mul-ℝ-Vector-Space r (mul-ℝ-Vector-Space s v)
+  associative-mul-ℝ-Vector-Space =
+    associative-mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  left-zero-law-mul-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝ zero-ℝ-Vector-Space
+  left-zero-law-mul-ℝ-Vector-Space =
+    left-zero-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  right-zero-law-mul-ℝ-Vector-Space :
+    (r : ℝ l1) →
+    mul-ℝ-Vector-Space r zero-ℝ-Vector-Space ＝ zero-ℝ-Vector-Space
+  right-zero-law-mul-ℝ-Vector-Space =
+    right-zero-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  left-negative-law-mul-ℝ-Vector-Space :
+    (r : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (neg-ℝ r) v ＝
+    neg-ℝ-Vector-Space (mul-ℝ-Vector-Space r v)
+  left-negative-law-mul-ℝ-Vector-Space =
+    left-negative-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  right-negative-law-mul-ℝ-Vector-Space :
+    (r : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space r (neg-ℝ-Vector-Space v) ＝
+    neg-ℝ-Vector-Space (mul-ℝ-Vector-Space r v)
+  right-negative-law-mul-ℝ-Vector-Space =
+    right-negative-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V
+
+  mul-neg-one-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ neg-ℝ-Vector-Space v
+  mul-neg-one-ℝ-Vector-Space =
+    mul-neg-one-Vector-Space (local-commutative-ring-ℝ l1) V
+```
+
+### The real numbers are a real vector space
+
+```agda
+real-vector-space-ℝ : (l : Level) → ℝ-Vector-Space l (lsuc l)
+real-vector-space-ℝ l =
+  vector-space-local-commutative-ring-Local-Commutative-Ring
+    ( local-commutative-ring-ℝ l)
+```
+
+## See also
+
+- [Vector spaces](linear-algebra.vector-spaces.md)
diff --git a/src/linear-algebra/vector-spaces.lagda.md b/src/linear-algebra/vector-spaces.lagda.md
new file mode 100644
index 0000000000..c7c658f41f
--- /dev/null
+++ b/src/linear-algebra/vector-spaces.lagda.md
@@ -0,0 +1,198 @@
+# Vector spaces
+
+```agda
+module linear-algebra.vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.local-commutative-rings
+
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.left-modules-commutative-rings
+```
+
+</details>
+
+## Idea
+
+A {{#concept "vector space" WD="vector space" WDID=Q125977}} is a
+[left module](linear-algebra.left-modules-rings.md) over a
+[local commutative ring](commutative-algebra.local-commutative-rings.md).
+
+## Definition
+
+```agda
+Vector-Space :
+  {l1 : Level} (l2 : Level) → Local-Commutative-Ring l1 → UU (l1 ⊔ lsuc l2)
+Vector-Space l2 R =
+  left-module-Commutative-Ring l2 (commutative-ring-Local-Commutative-Ring R)
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level} (R : Local-Commutative-Ring l1) (V : Vector-Space l2 R)
+  where
+
+  ab-Vector-Space : Ab l2
+  ab-Vector-Space =
+    ab-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  set-Vector-Space : Set l2
+  set-Vector-Space = set-Ab ab-Vector-Space
+
+  type-Vector-Space : UU l2
+  type-Vector-Space = type-Ab ab-Vector-Space
+
+  add-Vector-Space : type-Vector-Space → type-Vector-Space → type-Vector-Space
+  add-Vector-Space = add-Ab ab-Vector-Space
+
+  zero-Vector-Space : type-Vector-Space
+  zero-Vector-Space = zero-Ab ab-Vector-Space
+
+  neg-Vector-Space : type-Vector-Space → type-Vector-Space
+  neg-Vector-Space = neg-Ab ab-Vector-Space
+
+  mul-Vector-Space :
+    type-Local-Commutative-Ring R → type-Vector-Space → type-Vector-Space
+  mul-Vector-Space =
+    mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  associative-add-Vector-Space :
+    (v w x : type-Vector-Space) →
+    add-Vector-Space (add-Vector-Space v w) x ＝
+    add-Vector-Space v (add-Vector-Space w x)
+  associative-add-Vector-Space = associative-add-Ab ab-Vector-Space
+
+  left-unit-law-add-Vector-Space :
+    (v : type-Vector-Space) → add-Vector-Space zero-Vector-Space v ＝ v
+  left-unit-law-add-Vector-Space = left-unit-law-add-Ab ab-Vector-Space
+
+  right-unit-law-add-Vector-Space :
+    (v : type-Vector-Space) → add-Vector-Space v zero-Vector-Space ＝ v
+  right-unit-law-add-Vector-Space = right-unit-law-add-Ab ab-Vector-Space
+
+  left-inverse-law-add-Vector-Space :
+    (v : type-Vector-Space) →
+    add-Vector-Space (neg-Vector-Space v) v ＝ zero-Vector-Space
+  left-inverse-law-add-Vector-Space = left-inverse-law-add-Ab ab-Vector-Space
+
+  right-inverse-law-add-Vector-Space :
+    (v : type-Vector-Space) →
+    add-Vector-Space v (neg-Vector-Space v) ＝ zero-Vector-Space
+  right-inverse-law-add-Vector-Space = right-inverse-law-add-Ab ab-Vector-Space
+
+  commutative-add-Vector-Space :
+    (v w : type-Vector-Space) → add-Vector-Space v w ＝ add-Vector-Space w v
+  commutative-add-Vector-Space = commutative-add-Ab ab-Vector-Space
+
+  left-unit-law-mul-Vector-Space :
+    (v : type-Vector-Space) →
+    mul-Vector-Space (one-Local-Commutative-Ring R) v ＝ v
+  left-unit-law-mul-Vector-Space =
+    left-unit-law-mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  left-distributive-mul-add-Vector-Space :
+    (r : type-Local-Commutative-Ring R) (v w : type-Vector-Space) →
+    mul-Vector-Space r (add-Vector-Space v w) ＝
+    add-Vector-Space (mul-Vector-Space r v) (mul-Vector-Space r w)
+  left-distributive-mul-add-Vector-Space =
+    left-distributive-mul-add-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  right-distributive-mul-add-Vector-Space :
+    (r s : type-Local-Commutative-Ring R) (v : type-Vector-Space) →
+    mul-Vector-Space (add-Local-Commutative-Ring R r s) v ＝
+    add-Vector-Space (mul-Vector-Space r v) (mul-Vector-Space s v)
+  right-distributive-mul-add-Vector-Space =
+    right-distributive-mul-add-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  associative-mul-Vector-Space :
+    (r s : type-Local-Commutative-Ring R) (v : type-Vector-Space) →
+    mul-Vector-Space (mul-Local-Commutative-Ring R r s) v ＝
+    mul-Vector-Space r (mul-Vector-Space s v)
+  associative-mul-Vector-Space =
+    associative-mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  left-zero-law-mul-Vector-Space :
+    (v : type-Vector-Space) →
+    mul-Vector-Space (zero-Local-Commutative-Ring R) v ＝ zero-Vector-Space
+  left-zero-law-mul-Vector-Space =
+    left-zero-law-mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  right-zero-law-mul-Vector-Space :
+    (r : type-Local-Commutative-Ring R) →
+    mul-Vector-Space r zero-Vector-Space ＝ zero-Vector-Space
+  right-zero-law-mul-Vector-Space =
+    right-zero-law-mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  left-negative-law-mul-Vector-Space :
+    (r : type-Local-Commutative-Ring R) (v : type-Vector-Space) →
+    mul-Vector-Space (neg-Local-Commutative-Ring R r) v ＝
+    neg-Vector-Space (mul-Vector-Space r v)
+  left-negative-law-mul-Vector-Space =
+    left-negative-law-mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  right-negative-law-mul-Vector-Space :
+    (r : type-Local-Commutative-Ring R) (v : type-Vector-Space) →
+    mul-Vector-Space r (neg-Vector-Space v) ＝
+    neg-Vector-Space (mul-Vector-Space r v)
+  right-negative-law-mul-Vector-Space =
+    right-negative-law-mul-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+
+  mul-neg-one-Vector-Space :
+    (v : type-Vector-Space) →
+    mul-Vector-Space
+      ( neg-Local-Commutative-Ring R (one-Local-Commutative-Ring R))
+      ( v) ＝
+    neg-Vector-Space v
+  mul-neg-one-Vector-Space =
+    mul-neg-one-left-module-Commutative-Ring
+      ( commutative-ring-Local-Commutative-Ring R)
+      ( V)
+```
+
+### Any local commutative ring is a vector space over itself
+
+```agda
+vector-space-local-commutative-ring-Local-Commutative-Ring :
+  {l : Level} (R : Local-Commutative-Ring l) → Vector-Space l R
+vector-space-local-commutative-ring-Local-Commutative-Ring R =
+  left-module-commutative-ring-Commutative-Ring
+    ( commutative-ring-Local-Commutative-Ring R)
+```
+
+## See also
+
+- [Real vector spaces](linear-algebra.real-vector-spaces.md)
+
+## External links
+
+- [Vector space](https://en.wikipedia.org/wiki/Vector_space) on Wikipedia
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index f7b0c6a18d..665c66a59e 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -9,7 +9,9 @@ open import real-numbers.absolute-value-closed-intervals-real-numbers public
 open import real-numbers.absolute-value-real-numbers public
 open import real-numbers.accumulation-points-subsets-real-numbers public
 open import real-numbers.addition-lower-dedekind-real-numbers public
+open import real-numbers.addition-negative-real-numbers public
 open import real-numbers.addition-nonnegative-real-numbers public
+open import real-numbers.addition-nonzero-real-numbers public
 open import real-numbers.addition-positive-real-numbers public
 open import real-numbers.addition-real-numbers public
 open import real-numbers.addition-upper-dedekind-real-numbers public
@@ -46,6 +48,7 @@ open import real-numbers.large-multiplicative-monoid-of-real-numbers public
 open import real-numbers.large-ring-of-real-numbers public
 open import real-numbers.limits-sequences-real-numbers public
 open import real-numbers.lipschitz-continuity-multiplication-real-numbers public
+open import real-numbers.local-ring-of-real-numbers public
 open import real-numbers.located-metric-space-of-real-numbers public
 open import real-numbers.lower-dedekind-real-numbers public
 open import real-numbers.maximum-finite-families-real-numbers public
diff --git a/src/real-numbers/addition-negative-real-numbers.lagda.md b/src/real-numbers/addition-negative-real-numbers.lagda.md
new file mode 100644
index 0000000000..c3e3cef113
--- /dev/null
+++ b/src/real-numbers/addition-negative-real-numbers.lagda.md
@@ -0,0 +1,85 @@
+# Addition of negative real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.addition-negative-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.functoriality-disjunction
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import real-numbers.addition-positive-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.negative-real-numbers
+open import real-numbers.positive-and-negative-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+```
+
+</details>
+
+## Idea
+
+The [negative](real-numbers.negative-real-numbers.md)
+[real numbers](real-numbers.dedekind-real-numbers.md) are closed under
+[addition](real-numbers.addition-real-numbers.md).
+
+## Definition
+
+```agda
+abstract
+  is-negative-add-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → is-negative-ℝ x → is-negative-ℝ y →
+    is-negative-ℝ (x +ℝ y)
+  is-negative-add-ℝ {x = x} {y = y} x<0 y<0 =
+    transitive-le-ℝ
+      ( x +ℝ y)
+      ( x)
+      ( zero-ℝ)
+      ( x<0)
+      ( tr
+        ( le-ℝ (x +ℝ y))
+        ( right-unit-law-add-ℝ x)
+        ( preserves-le-left-add-ℝ x y zero-ℝ y<0))
+
+add-ℝ⁻ : {l1 l2 : Level} → ℝ⁻ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2)
+add-ℝ⁻ (x , x<0) (y , y<0) = (add-ℝ x y , is-negative-add-ℝ x<0 y<0)
+
+infixl 35 _+ℝ⁻_
+
+_+ℝ⁻_ : {l1 l2 : Level} → ℝ⁻ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2)
+_+ℝ⁻_ = add-ℝ⁻
+```
+
+## Properties
+
+### If `x + y` is negative, `x` or `y` is negative
+
+```agda
+abstract
+  is-negative-either-is-negative-add-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → is-negative-ℝ (x +ℝ y) →
+    disjunction-type (is-negative-ℝ x) (is-negative-ℝ y)
+  is-negative-either-is-negative-add-ℝ x y x+y<0 =
+    map-disjunction
+      ( is-negative-is-positive-neg-ℝ x)
+      ( is-negative-is-positive-neg-ℝ y)
+      ( is-positive-either-is-positive-add-ℝ
+        ( neg-ℝ x)
+        ( neg-ℝ y)
+        ( tr
+          ( is-positive-ℝ)
+          ( distributive-neg-add-ℝ x y)
+          ( neg-is-negative-ℝ (x +ℝ y) x+y<0)))
+```
diff --git a/src/real-numbers/addition-nonzero-real-numbers.lagda.md b/src/real-numbers/addition-nonzero-real-numbers.lagda.md
new file mode 100644
index 0000000000..e59f5b96f1
--- /dev/null
+++ b/src/real-numbers/addition-nonzero-real-numbers.lagda.md
@@ -0,0 +1,56 @@
+# Addition of nonzero real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.addition-nonzero-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.functoriality-disjunction
+open import foundation.universe-levels
+
+open import real-numbers.addition-negative-real-numbers
+open import real-numbers.addition-positive-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.nonzero-real-numbers
+```
+
+</details>
+
+## Idea
+
+On this page we describe properties of
+[addition](real-numbers.addition-real-numbers.md) of
+[nonzero](real-numbers.nonzero-real-numbers.md)
+[real numbers](real-numbers.dedekind-real-numbers.md).
+
+## Properties
+
+### If `x + y` is nonzero, `x` is nonzero or `y` is nonzero
+
+```agda
+abstract
+  is-nonzero-either-is-nonzero-add-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) →
+    is-nonzero-ℝ (x +ℝ y) →
+    disjunction-type (is-nonzero-ℝ x) (is-nonzero-ℝ y)
+  is-nonzero-either-is-nonzero-add-ℝ x y =
+    elim-disjunction
+      ( is-nonzero-prop-ℝ x ∨ is-nonzero-prop-ℝ y)
+      ( λ x+y<0 →
+        map-disjunction
+          ( inl-disjunction)
+          ( inl-disjunction)
+          ( is-negative-either-is-negative-add-ℝ x y x+y<0))
+      ( λ 0<x+y →
+        map-disjunction
+          ( inr-disjunction)
+          ( inr-disjunction)
+          ( is-positive-either-is-positive-add-ℝ x y 0<x+y))
+```
diff --git a/src/real-numbers/local-ring-of-real-numbers.lagda.md b/src/real-numbers/local-ring-of-real-numbers.lagda.md
new file mode 100644
index 0000000000..030a5b42de
--- /dev/null
+++ b/src/real-numbers/local-ring-of-real-numbers.lagda.md
@@ -0,0 +1,52 @@
+# The local ring of Dedekind real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.local-ring-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.local-commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.functoriality-disjunction
+open import foundation.universe-levels
+
+open import real-numbers.addition-nonzero-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.large-ring-of-real-numbers
+open import real-numbers.multiplicative-inverses-nonzero-real-numbers
+open import real-numbers.nonzero-real-numbers
+```
+
+</details>
+
+## Idea
+
+The [ring of real numbers](real-numbers.large-ring-of-real-numbers.md) is a
+[local](commutative-algebra.local-commutative-rings.md)
+[commutative ring](commutative-algebra.commutative-rings.md). Notably, this is
+one of the strongest alternatives for the concept of field that applies to the
+[Dedekind real numbers](real-numbers.dedekind-real-numbers.md) constructively.
+
+## Definition
+
+```agda
+is-local-commutative-ring-ℝ :
+  (l : Level) → is-local-Commutative-Ring (commutative-ring-ℝ l)
+is-local-commutative-ring-ℝ l x y is-invertible-x+y =
+  map-disjunction
+    ( is-invertible-is-nonzero-ℝ x)
+    ( is-invertible-is-nonzero-ℝ y)
+    ( is-nonzero-either-is-nonzero-add-ℝ
+      ( x)
+      ( y)
+      ( is-nonzero-is-invertible-ℝ (x +ℝ y) is-invertible-x+y))
+
+local-commutative-ring-ℝ : (l : Level) → Local-Commutative-Ring (lsuc l)
+local-commutative-ring-ℝ l =
+  ( commutative-ring-ℝ l , is-local-commutative-ring-ℝ l)
+```
diff --git a/src/real-numbers/multiplication-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplication-nonzero-real-numbers.lagda.md
index 5f6c869630..42ea33baba 100644
--- a/src/real-numbers/multiplication-nonzero-real-numbers.lagda.md
+++ b/src/real-numbers/multiplication-nonzero-real-numbers.lagda.md
@@ -9,18 +9,29 @@ module real-numbers.multiplication-nonzero-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import commutative-algebra.invertible-elements-commutative-rings
+
+open import foundation.cartesian-product-types
+open import foundation.conjunction
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.large-ring-of-real-numbers
 open import real-numbers.multiplication-negative-real-numbers
 open import real-numbers.multiplication-positive-and-negative-real-numbers
 open import real-numbers.multiplication-positive-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.multiplicative-inverses-nonzero-real-numbers
 open import real-numbers.nonzero-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 ```
 
 </details>
@@ -66,3 +77,76 @@ mul-nonzero-ℝ :
 mul-nonzero-ℝ (x , x#0) (y , y#0) =
   ( x *ℝ y , is-nonzero-mul-ℝ x#0 y#0)
 ```
+
+## Properties
+
+### If the product of two real numbers is nonzero, they are both nonzero
+
+```agda
+module _
+  {l1 l2 : Level}
+  (x : ℝ l1)
+  (y : ℝ l2)
+  where
+
+  abstract
+    is-nonzero-factors-is-nonzero-mul-ℝ :
+      is-nonzero-ℝ (x *ℝ y) → is-nonzero-ℝ x × is-nonzero-ℝ y
+    is-nonzero-factors-is-nonzero-mul-ℝ =
+      let
+        motive = is-nonzero-prop-ℝ x ∧ is-nonzero-prop-ℝ y
+      in
+        elim-disjunction
+          ( motive)
+          ( λ xy<0 →
+            elim-disjunction
+              ( motive)
+              ( map-product inr-disjunction inl-disjunction)
+              ( map-product inl-disjunction inr-disjunction)
+              ( different-signs-is-negative-mul-ℝ x y xy<0))
+          ( λ 0<xy →
+            elim-disjunction
+              ( motive)
+              ( map-product inl-disjunction inl-disjunction)
+              ( map-product inr-disjunction inr-disjunction)
+              ( same-sign-is-positive-mul-ℝ x y 0<xy))
+```
+
+### If a real number has a multiplicative inverse, it is nonzero
+
+```agda
+abstract
+  is-nonzero-has-right-inverse-mul-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → sim-ℝ (x *ℝ y) one-ℝ →
+    is-nonzero-ℝ x
+  is-nonzero-has-right-inverse-mul-ℝ x y xy=1 =
+    pr1
+      ( is-nonzero-factors-is-nonzero-mul-ℝ
+        ( x)
+        ( y)
+        ( is-nonzero-is-positive-ℝ
+          ( is-positive-sim-ℝ
+            ( symmetric-sim-ℝ xy=1)
+            ( is-positive-one-ℝ))))
+
+  is-nonzero-has-left-inverse-mul-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → sim-ℝ (x *ℝ y) one-ℝ →
+    is-nonzero-ℝ y
+  is-nonzero-has-left-inverse-mul-ℝ x y xy=1 =
+    is-nonzero-has-right-inverse-mul-ℝ y x
+      ( tr (λ z → sim-ℝ z one-ℝ) (commutative-mul-ℝ x y) xy=1)
+
+  is-nonzero-is-invertible-ℝ :
+    {l : Level} (x : ℝ l) →
+    is-invertible-element-Commutative-Ring (commutative-ring-ℝ l) x →
+    is-nonzero-ℝ x
+  is-nonzero-is-invertible-ℝ {l} x (y , xy=1 , _) =
+    is-nonzero-has-right-inverse-mul-ℝ x y
+      ( inv-tr
+        ( λ z → sim-ℝ z one-ℝ)
+        ( xy=1)
+        ( symmetric-sim-ℝ
+          { x = one-ℝ}
+          { y = raise-ℝ l one-ℝ}
+          ( sim-raise-ℝ l one-ℝ)))
+```
diff --git a/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md b/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md
index 353a564925..72de9d1ce9 100644
--- a/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md
+++ b/src/real-numbers/multiplication-positive-and-negative-real-numbers.lagda.md
@@ -1,20 +1,41 @@
 # Multiplication by positive, negative, and nonnegative real numbers
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module real-numbers.multiplication-positive-and-negative-real-numbers where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.multiplication-closed-intervals-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.conjunction
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-disjunction
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import order-theory.posets
+
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.multiplication-positive-real-numbers
 open import real-numbers.multiplication-real-numbers
+open import real-numbers.negation-real-numbers
 open import real-numbers.negative-real-numbers
+open import real-numbers.positive-and-negative-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.strict-inequality-real-numbers
@@ -70,3 +91,72 @@ mul-negative-positive-ℝ :
 mul-negative-positive-ℝ (x , is-neg-x) (y , is-pos-y) =
   ( x *ℝ y , is-negative-mul-negative-positive-ℝ is-neg-x is-pos-y)
 ```
+
+### If the product of two real numbers is positive, both are negative or both are positive
+
+```agda
+abstract opaque
+  unfolding mul-ℝ
+
+  same-sign-is-positive-mul-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → is-positive-ℝ (x *ℝ y) →
+    type-disjunction-Prop
+      ( is-negative-prop-ℝ x ∧ is-negative-prop-ℝ y)
+      ( is-positive-prop-ℝ x ∧ is-positive-prop-ℝ y)
+  same-sign-is-positive-mul-ℝ x y 0<xy =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( ( is-negative-prop-ℝ x ∧ is-negative-prop-ℝ y) ∨
+            ( is-positive-prop-ℝ x ∧ is-positive-prop-ℝ y))
+      open inequality-reasoning-Poset ℚ-Poset
+    in do
+      ( q⁺@(q , is-pos-q) , q<xy) ←
+        exists-ℚ⁺-in-lower-cut-is-positive-ℝ (x *ℝ y) 0<xy
+      ( ( ax<x<bx@([ax,bx]@((ax , bx) , _) , ax<x , x<bx) ,
+          ay<y<by@([ay,by]@((ay , by) , _) , ay<y , y<by)) ,
+          q<[ax,bx][ay,by]) ← q<xy
+      rec-coproduct
+        ( λ (_ , is-neg-bx , _ , is-neg-by) →
+          inl-disjunction
+            ( is-negative-exists-ℚ⁻-in-upper-cut-ℝ
+                ( x)
+                ( intro-exists (bx , is-neg-bx) x<bx) ,
+              is-negative-exists-ℚ⁻-in-upper-cut-ℝ
+                ( y)
+                ( intro-exists (by , is-neg-by) y<by)))
+        ( λ (is-pos-ax , _ , is-pos-ay , _) →
+          inr-disjunction
+            ( is-positive-exists-ℚ⁺-in-lower-cut-ℝ
+                ( x)
+                ( intro-exists (ax , is-pos-ax) ax<x) ,
+              is-positive-exists-ℚ⁺-in-lower-cut-ℝ
+                ( y)
+                ( intro-exists (ay , is-pos-ay) ay<y)))
+        ( same-sign-bounds-is-positive-lower-bound-mul-closed-interval-ℚ
+          ( [ax,bx])
+          ( [ay,by])
+          ( is-positive-le-ℚ⁺ q⁺ q<[ax,bx][ay,by]))
+```
+
+### If the product of two real numbers is negative, one is positive and the other negative
+
+```agda
+abstract
+  different-signs-is-negative-mul-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → is-negative-ℝ (x *ℝ y) →
+    type-disjunction-Prop
+      ( is-positive-prop-ℝ x ∧ is-negative-prop-ℝ y)
+      ( is-negative-prop-ℝ x ∧ is-positive-prop-ℝ y)
+  different-signs-is-negative-mul-ℝ x y xy<0 =
+    map-disjunction
+      ( map-product (is-positive-is-negative-neg-ℝ x) id)
+      ( map-product (is-negative-is-positive-neg-ℝ x) id)
+      ( same-sign-is-positive-mul-ℝ
+        ( neg-ℝ x)
+        ( y)
+        ( inv-tr
+          ( is-positive-ℝ)
+          ( left-negative-law-mul-ℝ x y)
+          ( neg-is-negative-ℝ (x *ℝ y) xy<0)))
+```
diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md
index aedb75f632..a07ffadc38 100644
--- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md
+++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md
@@ -148,70 +148,6 @@ is-invertible-is-nonzero-ℝ x x≠0 =
         ( left-inverse-law-mul-nonzero-ℝ (x , x≠0))))
 ```
 
-### If a real number has a multiplicative inverse, it is nonzero
-
-```agda
-abstract opaque
-  unfolding mul-ℝ real-ℚ sim-ℝ
-
-  is-nonzero-has-right-inverse-mul-ℝ :
-    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → sim-ℝ (x *ℝ y) one-ℝ →
-    is-nonzero-ℝ x
-  is-nonzero-has-right-inverse-mul-ℝ x y (_ , L1⊆Lxy) =
-    let open do-syntax-trunc-Prop (is-nonzero-prop-ℝ x)
-    in do
-      ( ( ([a,b]@((a , b) , a≤b) , a<x , x<b) ,
-          ([c,d]@((c , d) , c≤d) , c<y , y<d)) ,
-        0<[a,b][c,d]) ← L1⊆Lxy zero-ℚ le-zero-one-ℚ
-      let
-        is-positive-mul p q {r} lb1 lb2 =
-          is-positive-le-zero-ℚ
-            ( concatenate-le-leq-ℚ
-              ( zero-ℚ)
-              ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d])
-              ( p *ℚ q)
-              ( 0<[a,b][c,d])
-              ( transitive-leq-ℚ
-                ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d])
-                ( r)
-                ( p *ℚ q)
-                ( lb1)
-                ( lb2)))
-      rec-coproduct
-        ( λ (is-neg-a , is-neg-c) →
-          rec-coproduct
-            ( λ (is-neg-b , is-neg-d) →
-              inl-disjunction
-                ( is-negative-exists-ℚ⁻-in-upper-cut-ℝ
-                  ( x)
-                  ( intro-exists (b , is-neg-b) x<b)))
-            ( λ (is-pos-b , is-pos-d) →
-              ex-falso
-                ( is-not-negative-and-positive-ℚ
-                  ( is-negative-mul-negative-positive-ℚ is-neg-a is-pos-d ,
-                    is-positive-mul a d
-                      ( leq-right-min-ℚ _ _)
-                      ( leq-left-min-ℚ _ _))))
-            ( same-sign-is-positive-mul-ℚ
-              ( is-positive-mul b d
-                ( leq-right-min-ℚ _ _)
-                ( leq-right-min-ℚ _ _))))
-        ( λ (is-pos-a , is-pos-c) →
-          inr-disjunction
-            ( is-positive-exists-ℚ⁺-in-lower-cut-ℝ
-              ( x)
-              ( intro-exists (a , is-pos-a) a<x)))
-        ( same-sign-is-positive-mul-ℚ
-          ( is-positive-mul a c (leq-left-min-ℚ _ _) (leq-left-min-ℚ _ _)))
-
-  is-nonzero-has-left-inverse-mul-ℝ :
-    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → sim-ℝ (x *ℝ y) one-ℝ →
-    is-nonzero-ℝ y
-  is-nonzero-has-left-inverse-mul-ℝ x y xy=1 =
-    is-nonzero-has-right-inverse-mul-ℝ y x
-      ( tr (λ z → sim-ℝ z one-ℝ) (commutative-mul-ℝ _ _) xy=1)
-```
-
 ### The multiplicative inverse is unique
 
 ```agda
diff --git a/src/real-numbers/negative-real-numbers.lagda.md b/src/real-numbers/negative-real-numbers.lagda.md
index 75b3944778..ced2c41ca1 100644
--- a/src/real-numbers/negative-real-numbers.lagda.md
+++ b/src/real-numbers/negative-real-numbers.lagda.md
@@ -21,6 +21,7 @@ open import foundation.universe-levels
 
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
 
@@ -92,3 +93,13 @@ module _
       ( exists-ℚ⁻-in-upper-cut-is-negative-ℝ ,
         is-negative-exists-ℚ⁻-in-upper-cut-ℝ)
 ```
+
+### Being nonnegative is preserved by similarity
+
+```agda
+abstract
+  is-negative-sim-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
+    sim-ℝ x y → is-negative-ℝ x → is-negative-ℝ y
+  is-negative-sim-ℝ = preserves-le-left-sim-ℝ _ _ _
+```
diff --git a/src/real-numbers/nonzero-real-numbers.lagda.md b/src/real-numbers/nonzero-real-numbers.lagda.md
index 2513d40149..c3e30a8c08 100644
--- a/src/real-numbers/nonzero-real-numbers.lagda.md
+++ b/src/real-numbers/nonzero-real-numbers.lagda.md
@@ -13,6 +13,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.disjunction
+open import foundation.functoriality-disjunction
 open import foundation.identity-types
 open import foundation.propositional-truncations
 open import foundation.propositions
@@ -201,5 +202,16 @@ module _
                     ( nonnegative-square-ℝ x)
                     ( refl))
             ＝ abs-ℝ x by inv (eq-abs-sqrt-square-ℝ x))
-          ( is-positive-sqrt-ℝ⁺ (square-ℝ x , 0<x²)))
+          ( is-positive-sqrt-is-positive-ℝ⁰⁺ _ 0<x²))
+```
+
+### Being nonzero is preserved by similarity
+
+```agda
+abstract
+  is-nonzero-sim-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
+    sim-ℝ x y → is-nonzero-ℝ x → is-nonzero-ℝ y
+  is-nonzero-sim-ℝ x~y =
+    map-disjunction (is-negative-sim-ℝ x~y) (is-positive-sim-ℝ x~y)
 ```
diff --git a/src/real-numbers/positive-and-negative-real-numbers.lagda.md b/src/real-numbers/positive-and-negative-real-numbers.lagda.md
index 18f7f33b89..e5964a4b3d 100644
--- a/src/real-numbers/positive-and-negative-real-numbers.lagda.md
+++ b/src/real-numbers/positive-and-negative-real-numbers.lagda.md
@@ -9,7 +9,10 @@ module real-numbers.positive-and-negative-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.logical-equivalences
+open import foundation.negation
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
@@ -78,6 +81,38 @@ neg-ℝ⁻ : {l : Level} → ℝ⁻ l → ℝ⁺ l
 neg-ℝ⁻ (x , is-neg-x) = (neg-ℝ x , neg-is-negative-ℝ x is-neg-x)
 ```
 
+### A real number is negative if and only if its negation is positive
+
+```agda
+abstract
+  is-negative-is-positive-neg-ℝ :
+    {l : Level} (x : ℝ l) → is-positive-ℝ (neg-ℝ x) → is-negative-ℝ x
+  is-negative-is-positive-neg-ℝ x 0<-x =
+    tr is-negative-ℝ (neg-neg-ℝ x) (neg-is-positive-ℝ (neg-ℝ x) 0<-x)
+
+is-negative-iff-neg-is-positive-ℝ :
+  {l : Level} (x : ℝ l) → is-negative-ℝ x ↔ is-positive-ℝ (neg-ℝ x)
+is-negative-iff-neg-is-positive-ℝ x =
+  ( neg-is-negative-ℝ x ,
+    is-negative-is-positive-neg-ℝ x)
+```
+
+### A real number is positive if and only if its negation is negative
+
+```agda
+abstract
+  is-positive-is-negative-neg-ℝ :
+    {l : Level} (x : ℝ l) → is-negative-ℝ (neg-ℝ x) → is-positive-ℝ x
+  is-positive-is-negative-neg-ℝ x -x<0 =
+    tr is-positive-ℝ (neg-neg-ℝ x) (neg-is-negative-ℝ (neg-ℝ x) -x<0)
+
+is-positive-iff-neg-is-negative-ℝ :
+  {l : Level} (x : ℝ l) → is-positive-ℝ x ↔ is-negative-ℝ (neg-ℝ x)
+is-positive-iff-neg-is-negative-ℝ x =
+  ( neg-is-positive-ℝ x ,
+    is-positive-is-negative-neg-ℝ x)
+```
+
 ### If a nonnegative real number `x` is less than a real number `y`, `y` is positive
 
 ```agda
@@ -87,3 +122,13 @@ abstract
     is-positive-ℝ y
   is-positive-le-ℝ⁰⁺ (x , 0≤x) y = concatenate-leq-le-ℝ zero-ℝ x y 0≤x
 ```
+
+### Real numbers are not both negative and nonnegative
+
+```agda
+abstract
+  is-not-negative-and-nonnegative-ℝ :
+    {l : Level} {x : ℝ l} → ¬ (is-negative-ℝ x × is-nonnegative-ℝ x)
+  is-not-negative-and-nonnegative-ℝ {x = x} (x<0 , 0≤x) =
+    not-leq-le-ℝ x zero-ℝ x<0 0≤x
+```
diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md
index e0b81e741e..d00d7fc4b6 100644
--- a/src/real-numbers/positive-real-numbers.lagda.md
+++ b/src/real-numbers/positive-real-numbers.lagda.md
@@ -85,9 +85,9 @@ is-positive-real-ℝ⁺ = pr2
 abstract
   is-positive-sim-ℝ :
     {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
-    is-positive-ℝ x → sim-ℝ x y → is-positive-ℝ y
-  is-positive-sim-ℝ {x = x} {y = y} 0<x x~y =
-    preserves-le-right-sim-ℝ zero-ℝ x y x~y 0<x
+    sim-ℝ x y → is-positive-ℝ x → is-positive-ℝ y
+  is-positive-sim-ℝ {x = x} {y = y} =
+    preserves-le-right-sim-ℝ zero-ℝ x y
 ```
 
 ### Dedekind cuts of positive real numbers
@@ -251,6 +251,9 @@ positive-real-ℚ⁺ (q , pos-q) = (real-ℚ q , preserves-is-positive-real-ℚ
 
 one-ℝ⁺ : ℝ⁺ lzero
 one-ℝ⁺ = positive-real-ℚ⁺ one-ℚ⁺
+
+is-positive-one-ℝ : is-positive-ℝ one-ℝ
+is-positive-one-ℝ = is-positive-real-ℝ⁺ one-ℝ⁺
 ```
 
 ### `x` is positive if and only if there exists a positive rational number it is not less than or equal to
diff --git a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md
index d7c62f6516..117bd2589a 100644
--- a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md
+++ b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md
@@ -51,6 +51,7 @@ open import foundation.universe-levels
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.inequality-real-numbers
 open import real-numbers.multiplication-nonnegative-real-numbers
+open import real-numbers.multiplication-positive-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.nonnegative-real-numbers
 open import real-numbers.positive-and-negative-real-numbers
@@ -651,20 +652,37 @@ abstract
                         ( is-section-square-ℝ⁰⁺ y)))))))
 ```
 
-### The square root of a positive real number is positive
+### The square root of a nonnegative real number is positive if and only if the real number is positive
 
 ```agda
 abstract opaque
   unfolding real-sqrt-ℝ⁰⁺
 
-  is-positive-sqrt-ℝ⁺ :
-    {l : Level} (x : ℝ⁺ l) → is-positive-ℝ (real-sqrt-ℝ⁰⁺ (nonnegative-ℝ⁺ x))
-  is-positive-sqrt-ℝ⁺ x⁺@(x , _) =
+  is-positive-sqrt-is-positive-ℝ⁰⁺ :
+    {l : Level} (x : ℝ⁰⁺ l) → is-positive-ℝ (real-ℝ⁰⁺ x) →
+    is-positive-ℝ (real-sqrt-ℝ⁰⁺ x)
+  is-positive-sqrt-is-positive-ℝ⁰⁺ x⁰⁺@(x , _) 0<x =
     is-positive-zero-in-lower-cut-ℝ
-      ( real-sqrt-ℝ⁰⁺ (nonnegative-ℝ⁺ x⁺))
+      ( real-sqrt-ℝ⁰⁺ x⁰⁺)
       ( λ _ →
         inv-tr
           ( is-in-lower-cut-ℝ x)
           ( left-zero-law-mul-ℚ zero-ℚ)
-          ( zero-in-lower-cut-ℝ⁺ x⁺))
+          ( zero-in-lower-cut-ℝ⁺ (x , 0<x)))
+
+  is-positive-is-positive-sqrt-ℝ⁰⁺ :
+    {l : Level} (x : ℝ⁰⁺ l) →
+    is-positive-ℝ (real-sqrt-ℝ⁰⁺ x) → is-positive-ℝ (real-ℝ⁰⁺ x)
+  is-positive-is-positive-sqrt-ℝ⁰⁺ x⁰⁺@(x , _) 0<√x =
+    tr
+      ( is-positive-ℝ)
+      ( eq-real-square-sqrt-ℝ⁰⁺ x⁰⁺)
+      ( is-positive-mul-ℝ 0<√x 0<√x)
+
+is-positive-sqrt-iff-is-positive-ℝ⁰⁺ :
+  {l : Level} (x : ℝ⁰⁺ l) →
+  is-positive-ℝ (real-sqrt-ℝ⁰⁺ x) ↔ is-positive-ℝ (real-ℝ⁰⁺ x)
+is-positive-sqrt-iff-is-positive-ℝ⁰⁺ x =
+  ( is-positive-is-positive-sqrt-ℝ⁰⁺ x ,
+    is-positive-sqrt-is-positive-ℝ⁰⁺ x)
 ```
diff --git a/src/real-numbers/squares-real-numbers.lagda.md b/src/real-numbers/squares-real-numbers.lagda.md
index d64d870327..15ad604956 100644
--- a/src/real-numbers/squares-real-numbers.lagda.md
+++ b/src/real-numbers/squares-real-numbers.lagda.md
@@ -46,6 +46,7 @@ open import real-numbers.nonnegative-real-numbers
 open import real-numbers.positive-and-negative-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 open import real-numbers.strict-inequality-nonnegative-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
@@ -354,3 +355,21 @@ abstract
       ＝ square-ℝ x -ℝ real-ℕ 2 *ℝ (x *ℝ y) +ℝ square-ℝ y
         by ap-add-ℝ (ap-add-ℝ refl (right-negative-law-mul-ℝ _ _)) refl
 ```
+
+### Squaring preserves similarity
+
+```agda
+abstract
+  preserves-sim-square-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
+    sim-ℝ x y → sim-ℝ (square-ℝ x) (square-ℝ y)
+  preserves-sim-square-ℝ x~y = preserves-sim-mul-ℝ x~y x~y
+```
+
+### `0² = 0`
+
+```agda
+abstract
+  square-zero-ℝ : square-ℝ zero-ℝ ＝ zero-ℝ
+  square-zero-ℝ = eq-sim-ℝ (left-zero-law-mul-ℝ zero-ℝ)
+```