diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index 9c1cd311ee..240d62913f 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.bilinear-forms-real-vector-spaces public
 open import linear-algebra.complex-vector-spaces public
 open import linear-algebra.constant-matrices public
 open import linear-algebra.constant-tuples public
@@ -33,14 +34,18 @@ open import linear-algebra.linear-spans-left-modules-rings public
 open import linear-algebra.matrices public
 open import linear-algebra.matrices-on-rings public
 open import linear-algebra.multiplication-matrices public
+open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public
+open import linear-algebra.orthogonality-real-inner-product-spaces 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-inner-product-spaces 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
 open import linear-algebra.scalar-multiplication-tuples-on-rings public
 open import linear-algebra.subsets-left-modules-rings public
+open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
 open import linear-algebra.transposition-matrices public
 open import linear-algebra.tuples-on-commutative-monoids public
 open import linear-algebra.tuples-on-commutative-rings public
diff --git a/src/linear-algebra/bilinear-forms-real-vector-spaces.lagda.md b/src/linear-algebra/bilinear-forms-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..613a5182a2
--- /dev/null
+++ b/src/linear-algebra/bilinear-forms-real-vector-spaces.lagda.md
@@ -0,0 +1,178 @@
+# Bilinear forms in real vector spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.bilinear-forms-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import linear-algebra.real-vector-spaces
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.multiplication-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "bilinear form" WDID=Q837924 WD="bilinear form" Disambiguation="on a real vector space" Agda=bilinear-form-ℝ-Vector-Space}}
+on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a map
+`B : V → V → ℝ` that is linear in each argument:
+`B (a * x + b * y) z = a * B x z + b * B y z` and
+`B x (a * y + b * z) = a * B x y + b * B x z`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (B : type-ℝ-Vector-Space V → type-ℝ-Vector-Space V → ℝ l1)
+  where
+
+  is-left-additive-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-left-additive-prop-form-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ x →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ y →
+            Π-Prop
+              ( type-ℝ-Vector-Space V)
+              ( λ z →
+                Id-Prop
+                  ( ℝ-Set l1)
+                  ( B (add-ℝ-Vector-Space V x y) z)
+                  ( B x z +ℝ B y z))))
+
+  is-left-additive-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-left-additive-form-ℝ-Vector-Space =
+    type-Prop is-left-additive-prop-form-ℝ-Vector-Space
+
+  preserves-scalar-mul-left-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  preserves-scalar-mul-left-prop-form-ℝ-Vector-Space =
+    Π-Prop
+      ( ℝ l1)
+      ( λ a →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ x →
+            Π-Prop
+              ( type-ℝ-Vector-Space V)
+              ( λ y →
+                Id-Prop
+                  ( ℝ-Set l1)
+                  ( B (mul-ℝ-Vector-Space V a x) y)
+                  ( a *ℝ B x y))))
+
+  preserves-scalar-mul-left-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  preserves-scalar-mul-left-form-ℝ-Vector-Space =
+    type-Prop preserves-scalar-mul-left-prop-form-ℝ-Vector-Space
+
+  is-right-additive-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-right-additive-prop-form-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ x →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ y →
+            Π-Prop
+              ( type-ℝ-Vector-Space V)
+              ( λ z →
+                Id-Prop
+                  ( ℝ-Set l1)
+                  ( B x (add-ℝ-Vector-Space V y z))
+                  ( B x y +ℝ B x z))))
+
+  is-right-additive-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-right-additive-form-ℝ-Vector-Space =
+    type-Prop is-right-additive-prop-form-ℝ-Vector-Space
+
+  preserves-scalar-mul-right-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  preserves-scalar-mul-right-prop-form-ℝ-Vector-Space =
+    Π-Prop
+      ( ℝ l1)
+      ( λ a →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ x →
+            Π-Prop
+              ( type-ℝ-Vector-Space V)
+              ( λ y →
+                Id-Prop
+                  ( ℝ-Set l1)
+                  ( B x (mul-ℝ-Vector-Space V a y))
+                  ( a *ℝ B x y))))
+
+  preserves-scalar-mul-right-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  preserves-scalar-mul-right-form-ℝ-Vector-Space =
+    type-Prop preserves-scalar-mul-right-prop-form-ℝ-Vector-Space
+
+  is-bilinear-prop-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-bilinear-prop-form-ℝ-Vector-Space =
+    is-left-additive-prop-form-ℝ-Vector-Space ∧
+    preserves-scalar-mul-left-prop-form-ℝ-Vector-Space ∧
+    is-right-additive-prop-form-ℝ-Vector-Space ∧
+    preserves-scalar-mul-right-prop-form-ℝ-Vector-Space
+
+  is-bilinear-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-bilinear-form-ℝ-Vector-Space =
+    type-Prop is-bilinear-prop-form-ℝ-Vector-Space
+
+bilinear-form-ℝ-Vector-Space :
+  {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) → UU (lsuc l1 ⊔ l2)
+bilinear-form-ℝ-Vector-Space V =
+  type-subtype (is-bilinear-prop-form-ℝ-Vector-Space V)
+
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (B : bilinear-form-ℝ-Vector-Space V)
+  where
+
+  map-bilinear-form-ℝ-Vector-Space :
+    type-ℝ-Vector-Space V → type-ℝ-Vector-Space V → ℝ l1
+  map-bilinear-form-ℝ-Vector-Space = pr1 B
+
+  is-left-additive-map-bilinear-form-ℝ-Vector-Space :
+    is-left-additive-form-ℝ-Vector-Space V map-bilinear-form-ℝ-Vector-Space
+  is-left-additive-map-bilinear-form-ℝ-Vector-Space = pr1 (pr2 B)
+
+  preserves-scalar-mul-left-map-bilinear-form-ℝ-Vector-Space :
+    preserves-scalar-mul-left-form-ℝ-Vector-Space
+      ( V)
+      ( map-bilinear-form-ℝ-Vector-Space)
+  preserves-scalar-mul-left-map-bilinear-form-ℝ-Vector-Space = pr1 (pr2 (pr2 B))
+
+  is-right-additive-map-bilinear-form-ℝ-Vector-Space :
+    is-right-additive-form-ℝ-Vector-Space
+      ( V)
+      ( map-bilinear-form-ℝ-Vector-Space)
+  is-right-additive-map-bilinear-form-ℝ-Vector-Space = pr1 (pr2 (pr2 (pr2 B)))
+
+  preserves-scalar-mul-right-map-bilinear-form-ℝ-Vector-Space :
+    preserves-scalar-mul-right-form-ℝ-Vector-Space
+      ( V)
+      ( map-bilinear-form-ℝ-Vector-Space)
+  preserves-scalar-mul-right-map-bilinear-form-ℝ-Vector-Space =
+    pr2 (pr2 (pr2 (pr2 B)))
+```
+
+## External links
+
+- [Bilinear form](https://en.wikipedia.org/wiki/Bilinear_form) on Wikipedia
diff --git a/src/linear-algebra/orthogonality-bilinear-forms-real-vector-spaces.lagda.md b/src/linear-algebra/orthogonality-bilinear-forms-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..c19fdedebf
--- /dev/null
+++ b/src/linear-algebra/orthogonality-bilinear-forms-real-vector-spaces.lagda.md
@@ -0,0 +1,54 @@
+# Orthogonality relative to a bilinear form in a real vector space
+
+```agda
+module linear-algebra.orthogonality-bilinear-forms-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import linear-algebra.bilinear-forms-real-vector-spaces
+open import linear-algebra.real-vector-spaces
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+Two elements `u` and `v` of a
+[real vector space](linear-algebra.real-vector-spaces.md) `V` are
+{{#concept "orthogonal" Disambiguation="relative to a bilinear form over a real vector space" Agda=is-orthogonal-bilinear-form-ℝ-Vector-Space}}
+relative to a
+[bilinear form](linear-algebra.bilinear-forms-real-vector-spaces.md)
+`B : V → V → ℝ` if `B u v = 0`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (B : bilinear-form-ℝ-Vector-Space V)
+  where
+
+  is-orthogonal-prop-bilinear-form-ℝ-Vector-Space :
+    Relation-Prop (lsuc l1) (type-ℝ-Vector-Space V)
+  is-orthogonal-prop-bilinear-form-ℝ-Vector-Space v w =
+    Id-Prop
+      ( ℝ-Set l1)
+      ( map-bilinear-form-ℝ-Vector-Space V B v w)
+      ( raise-zero-ℝ l1)
+
+  is-orthogonal-bilinear-form-ℝ-Vector-Space :
+    Relation (lsuc l1) (type-ℝ-Vector-Space V)
+  is-orthogonal-bilinear-form-ℝ-Vector-Space =
+    type-Relation-Prop is-orthogonal-prop-bilinear-form-ℝ-Vector-Space
+```
diff --git a/src/linear-algebra/orthogonality-real-inner-product-spaces.lagda.md b/src/linear-algebra/orthogonality-real-inner-product-spaces.lagda.md
new file mode 100644
index 0000000000..0c789e7018
--- /dev/null
+++ b/src/linear-algebra/orthogonality-real-inner-product-spaces.lagda.md
@@ -0,0 +1,132 @@
+# Orthogonality in real inner product spaces
+
+```agda
+module linear-algebra.orthogonality-real-inner-product-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces
+open import linear-algebra.real-inner-product-spaces
+
+open import real-numbers.addition-nonnegative-real-numbers
+open import real-numbers.addition-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.nonnegative-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
+open import real-numbers.square-roots-nonnegative-real-numbers
+```
+
+</details>
+
+## Idea
+
+Two vectors are
+{{#concept "orthogonal" WDID=Q215067 WD="orthogonality" Agda=is-orthogonal-ℝ-Inner-Product-Space  Disambiguation="in a real inner product space"}}
+in a [real inner product space](linear-algebra.real-inner-product-spaces.md) if
+they are
+[orthogonal](linear-algebra.orthogonality-bilinear-forms-real-vector-spaces.md)
+relative to the inner product as a
+[bilinear form](linear-algebra.bilinear-forms-real-vector-spaces.md).
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  is-orthogonal-prop-ℝ-Inner-Product-Space :
+    Relation-Prop (lsuc l1) (type-ℝ-Inner-Product-Space V)
+  is-orthogonal-prop-ℝ-Inner-Product-Space =
+    is-orthogonal-prop-bilinear-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space V)
+      ( bilinear-form-inner-product-ℝ-Inner-Product-Space V)
+
+  is-orthogonal-ℝ-Inner-Product-Space :
+    Relation (lsuc l1) (type-ℝ-Inner-Product-Space V)
+  is-orthogonal-ℝ-Inner-Product-Space =
+    type-Relation-Prop is-orthogonal-prop-ℝ-Inner-Product-Space
+```
+
+## Properties
+
+### The Pythagorean Theorem
+
+The Pythagorean theorem for real inner product spaces asserts that for
+orthogonal `v` and `w`, the squared norm of `v + w` is the sum of the squared
+norm of `v` and the squared norm of `w`.
+
+The Pythagorean theorem is the [4th](literature.100-theorems.md#4) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
+## Proof
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  abstract
+    pythagorean-theorem-ℝ-Inner-Product-Space :
+      (v w : type-ℝ-Inner-Product-Space V) →
+      is-orthogonal-ℝ-Inner-Product-Space V v w →
+      squared-norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V v w) ＝
+      squared-norm-ℝ-Inner-Product-Space V v +ℝ
+      squared-norm-ℝ-Inner-Product-Space V w
+    pythagorean-theorem-ℝ-Inner-Product-Space v w v∙w=0 =
+      let
+        ⟨_,V_⟩ = inner-product-ℝ-Inner-Product-Space V
+        _+V_ = add-ℝ-Inner-Product-Space V
+      in
+        equational-reasoning
+          ⟨ v +V w ,V v +V w ⟩
+          ＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ ⟨ v ,V w ⟩ +ℝ ⟨ w ,V w ⟩
+            by squared-norm-add-ℝ-Inner-Product-Space V v w
+          ＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ raise-ℝ l1 zero-ℝ +ℝ ⟨ w ,V w ⟩
+            by ap-add-ℝ (ap-add-ℝ refl (ap-mul-ℝ refl v∙w=0)) refl
+          ＝ ⟨ v ,V v ⟩ +ℝ zero-ℝ +ℝ ⟨ w ,V w ⟩
+            by
+              ap-add-ℝ
+                ( eq-sim-ℝ
+                  ( preserves-sim-left-add-ℝ _ _ _
+                    ( similarity-reasoning-ℝ
+                      real-ℕ 2 *ℝ raise-ℝ l1 zero-ℝ
+                      ~ℝ real-ℕ 2 *ℝ zero-ℝ
+                        by
+                          preserves-sim-left-mul-ℝ _ _ _
+                            ( sim-raise-ℝ' l1 zero-ℝ)
+                      ~ℝ zero-ℝ
+                        by right-zero-law-mul-ℝ _)))
+                ( refl)
+          ＝ ⟨ v ,V v ⟩ +ℝ ⟨ w ,V w ⟩
+            by ap-add-ℝ (right-unit-law-add-ℝ _) refl
+
+    norm-add-orthogonal-ℝ-Inner-Product-Space :
+      (v w : type-ℝ-Inner-Product-Space V) →
+      is-orthogonal-ℝ-Inner-Product-Space V v w →
+      norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V v w) ＝
+      real-sqrt-ℝ⁰⁺
+        ( nonnegative-squared-norm-ℝ-Inner-Product-Space V v +ℝ⁰⁺
+          nonnegative-squared-norm-ℝ-Inner-Product-Space V w)
+    norm-add-orthogonal-ℝ-Inner-Product-Space v w v∙w=0 =
+      ap
+        ( real-sqrt-ℝ⁰⁺)
+        ( eq-ℝ⁰⁺ _ _
+          ( pythagorean-theorem-ℝ-Inner-Product-Space v w v∙w=0))
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/linear-algebra/real-inner-product-spaces.lagda.md b/src/linear-algebra/real-inner-product-spaces.lagda.md
new file mode 100644
index 0000000000..622da1fb0f
--- /dev/null
+++ b/src/linear-algebra/real-inner-product-spaces.lagda.md
@@ -0,0 +1,381 @@
+# Real inner product spaces
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module linear-algebra.real-inner-product-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import linear-algebra.bilinear-forms-real-vector-spaces
+open import linear-algebra.real-vector-spaces
+open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.extensionality-multiplication-bilinear-form-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.raising-universe-levels-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
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "inner product" WDID=Q23924662 WD="inner product" Disambiguation="on a real vector space" Agda=inner-product-ℝ-Vector-Space}}
+on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a
+[symmetric](linear-algebra.symmetric-bilinear-forms-real-vector-spaces.md)
+[bilinear form](linear-algebra.bilinear-forms-real-vector-spaces.md)
+`i : V → V → ℝ` such that for all `v : V`, `i v v` is
+[nonnegative](real-numbers.nonnegative-real-numbers.md), and if `i v v = 0`,
+then `v` is the zero vector.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (B : bilinear-form-ℝ-Vector-Space V)
+  where
+
+  is-semidefinite-prop-bilinear-form-ℝ-Vector-Space : Prop (l1 ⊔ l2)
+  is-semidefinite-prop-bilinear-form-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ v → is-nonnegative-prop-ℝ (map-bilinear-form-ℝ-Vector-Space V B v v))
+
+  is-extensional-prop-bilinear-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-extensional-prop-bilinear-form-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ v →
+        hom-Prop
+          ( Id-Prop
+            ( ℝ-Set l1)
+            ( map-bilinear-form-ℝ-Vector-Space V B v v)
+            ( raise-ℝ l1 zero-ℝ))
+          ( is-zero-prop-ℝ-Vector-Space V v))
+
+  is-inner-product-prop-bilinear-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-inner-product-prop-bilinear-form-ℝ-Vector-Space =
+    is-symmetric-prop-bilinear-form-ℝ-Vector-Space V B ∧
+    is-semidefinite-prop-bilinear-form-ℝ-Vector-Space ∧
+    is-extensional-prop-bilinear-form-ℝ-Vector-Space
+
+  is-inner-product-bilinear-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-inner-product-bilinear-form-ℝ-Vector-Space =
+    type-Prop is-inner-product-prop-bilinear-form-ℝ-Vector-Space
+
+inner-product-ℝ-Vector-Space :
+  {l1 l2 : Level} → ℝ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2)
+inner-product-ℝ-Vector-Space V =
+  type-subtype (is-inner-product-prop-bilinear-form-ℝ-Vector-Space V)
+
+ℝ-Inner-Product-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+ℝ-Inner-Product-Space l1 l2 =
+  Σ (ℝ-Vector-Space l1 l2) inner-product-ℝ-Vector-Space
+
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  vector-space-ℝ-Inner-Product-Space : ℝ-Vector-Space l1 l2
+  vector-space-ℝ-Inner-Product-Space = pr1 V
+
+  bilinear-form-inner-product-ℝ-Inner-Product-Space :
+    bilinear-form-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+  bilinear-form-inner-product-ℝ-Inner-Product-Space = pr1 (pr2 V)
+
+  type-ℝ-Inner-Product-Space : UU l2
+  type-ℝ-Inner-Product-Space =
+    type-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  inner-product-ℝ-Inner-Product-Space :
+    type-ℝ-Inner-Product-Space → type-ℝ-Inner-Product-Space → ℝ l1
+  inner-product-ℝ-Inner-Product-Space =
+    map-bilinear-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( bilinear-form-inner-product-ℝ-Inner-Product-Space)
+
+  zero-ℝ-Inner-Product-Space : type-ℝ-Inner-Product-Space
+  zero-ℝ-Inner-Product-Space =
+    zero-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  is-zero-prop-ℝ-Inner-Product-Space : subtype l2 type-ℝ-Inner-Product-Space
+  is-zero-prop-ℝ-Inner-Product-Space =
+    is-zero-prop-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  is-zero-ℝ-Inner-Product-Space : type-ℝ-Inner-Product-Space → UU l2
+  is-zero-ℝ-Inner-Product-Space =
+    is-zero-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  add-ℝ-Inner-Product-Space :
+    type-ℝ-Inner-Product-Space → type-ℝ-Inner-Product-Space →
+    type-ℝ-Inner-Product-Space
+  add-ℝ-Inner-Product-Space =
+    add-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  neg-ℝ-Inner-Product-Space :
+    type-ℝ-Inner-Product-Space → type-ℝ-Inner-Product-Space
+  neg-ℝ-Inner-Product-Space =
+    neg-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  diff-ℝ-Inner-Product-Space :
+    type-ℝ-Inner-Product-Space → type-ℝ-Inner-Product-Space →
+    type-ℝ-Inner-Product-Space
+  diff-ℝ-Inner-Product-Space =
+    diff-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  mul-ℝ-Inner-Product-Space :
+    ℝ l1 → type-ℝ-Inner-Product-Space → type-ℝ-Inner-Product-Space
+  mul-ℝ-Inner-Product-Space =
+    mul-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+
+  is-left-additive-inner-product-ℝ-Inner-Product-Space :
+    is-left-additive-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( inner-product-ℝ-Inner-Product-Space)
+  is-left-additive-inner-product-ℝ-Inner-Product-Space =
+    is-left-additive-map-bilinear-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( bilinear-form-inner-product-ℝ-Inner-Product-Space)
+
+  is-left-homogeneous-inner-product-ℝ-Inner-Product-Space :
+    preserves-scalar-mul-left-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( inner-product-ℝ-Inner-Product-Space)
+  is-left-homogeneous-inner-product-ℝ-Inner-Product-Space =
+    preserves-scalar-mul-left-map-bilinear-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( bilinear-form-inner-product-ℝ-Inner-Product-Space)
+
+  is-right-additive-inner-product-ℝ-Inner-Product-Space :
+    is-right-additive-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( inner-product-ℝ-Inner-Product-Space)
+  is-right-additive-inner-product-ℝ-Inner-Product-Space =
+    is-right-additive-map-bilinear-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( bilinear-form-inner-product-ℝ-Inner-Product-Space)
+
+  is-right-homogeneous-inner-product-ℝ-Inner-Product-Space :
+    preserves-scalar-mul-right-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( inner-product-ℝ-Inner-Product-Space)
+  is-right-homogeneous-inner-product-ℝ-Inner-Product-Space =
+    preserves-scalar-mul-right-map-bilinear-form-ℝ-Vector-Space
+      ( vector-space-ℝ-Inner-Product-Space)
+      ( bilinear-form-inner-product-ℝ-Inner-Product-Space)
+
+  is-nonnegative-diagonal-inner-product-ℝ-Inner-Product-Space :
+    (v : type-ℝ-Inner-Product-Space) →
+    is-nonnegative-ℝ (inner-product-ℝ-Inner-Product-Space v v)
+  is-nonnegative-diagonal-inner-product-ℝ-Inner-Product-Space =
+    pr1 (pr2 (pr2 (pr2 V)))
+
+  is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space :
+    (v : type-ℝ-Inner-Product-Space) →
+    inner-product-ℝ-Inner-Product-Space v v ＝ raise-zero-ℝ l1 →
+    v ＝ zero-ℝ-Inner-Product-Space
+  is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space =
+    pr2 (pr2 (pr2 (pr2 V)))
+
+  symmetric-inner-product-ℝ-Inner-Product-Space :
+    (v w : type-ℝ-Inner-Product-Space) →
+    inner-product-ℝ-Inner-Product-Space v w ＝
+    inner-product-ℝ-Inner-Product-Space w v
+  symmetric-inner-product-ℝ-Inner-Product-Space = pr1 (pr2 (pr2 V))
+
+  nonnegative-squared-norm-ℝ-Inner-Product-Space :
+    type-ℝ-Inner-Product-Space → ℝ⁰⁺ l1
+  nonnegative-squared-norm-ℝ-Inner-Product-Space v =
+    ( inner-product-ℝ-Inner-Product-Space v v ,
+      is-nonnegative-diagonal-inner-product-ℝ-Inner-Product-Space v)
+
+  squared-norm-ℝ-Inner-Product-Space : type-ℝ-Inner-Product-Space → ℝ l1
+  squared-norm-ℝ-Inner-Product-Space v =
+    real-ℝ⁰⁺ (nonnegative-squared-norm-ℝ-Inner-Product-Space v)
+
+  nonnegative-norm-ℝ-Inner-Product-Space : type-ℝ-Inner-Product-Space → ℝ⁰⁺ l1
+  nonnegative-norm-ℝ-Inner-Product-Space v =
+    sqrt-ℝ⁰⁺ (nonnegative-squared-norm-ℝ-Inner-Product-Space v)
+
+  norm-ℝ-Inner-Product-Space : type-ℝ-Inner-Product-Space → ℝ l1
+  norm-ℝ-Inner-Product-Space v =
+    real-ℝ⁰⁺ (nonnegative-norm-ℝ-Inner-Product-Space v)
+
+  mul-neg-one-ℝ-Inner-Product-Space :
+    (v : type-ℝ-Inner-Product-Space) →
+    mul-ℝ-Inner-Product-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝
+    neg-ℝ-Inner-Product-Space v
+  mul-neg-one-ℝ-Inner-Product-Space =
+    mul-neg-one-ℝ-Vector-Space vector-space-ℝ-Inner-Product-Space
+```
+
+## Properties
+
+### Negative laws of the inner product
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  abstract
+    right-negative-law-inner-product-ℝ-Inner-Product-Space :
+      (v w : type-ℝ-Inner-Product-Space V) →
+      inner-product-ℝ-Inner-Product-Space V v (neg-ℝ-Inner-Product-Space V w) ＝
+      neg-ℝ (inner-product-ℝ-Inner-Product-Space V v w)
+    right-negative-law-inner-product-ℝ-Inner-Product-Space v w =
+      equational-reasoning
+        inner-product-ℝ-Inner-Product-Space V v (neg-ℝ-Inner-Product-Space V w)
+        ＝
+          inner-product-ℝ-Inner-Product-Space
+            ( V)
+            ( v)
+            ( mul-ℝ-Inner-Product-Space
+              ( V)
+              ( neg-ℝ (raise-ℝ l1 one-ℝ))
+              ( w))
+          by
+            ap
+              ( inner-product-ℝ-Inner-Product-Space V v)
+              ( inv (mul-neg-one-ℝ-Inner-Product-Space V w))
+        ＝
+          neg-ℝ (raise-ℝ l1 one-ℝ) *ℝ
+          inner-product-ℝ-Inner-Product-Space V v w
+          by is-right-homogeneous-inner-product-ℝ-Inner-Product-Space V _ _ _
+        ＝
+          neg-ℝ (raise-ℝ l1 one-ℝ *ℝ inner-product-ℝ-Inner-Product-Space V v w)
+          by left-negative-law-mul-ℝ _ _
+        ＝
+          neg-ℝ (one-ℝ *ℝ inner-product-ℝ-Inner-Product-Space V v w)
+          by
+            ap
+              ( neg-ℝ)
+              ( eq-sim-ℝ
+                ( preserves-sim-right-mul-ℝ _ _ _ (sim-raise-ℝ' l1 one-ℝ)))
+        ＝ neg-ℝ (inner-product-ℝ-Inner-Product-Space V v w)
+          by ap neg-ℝ (left-unit-law-mul-ℝ _)
+
+    left-negative-law-inner-product-ℝ-Inner-Product-Space :
+      (v w : type-ℝ-Inner-Product-Space V) →
+      inner-product-ℝ-Inner-Product-Space V (neg-ℝ-Inner-Product-Space V v) w ＝
+      neg-ℝ (inner-product-ℝ-Inner-Product-Space V v w)
+    left-negative-law-inner-product-ℝ-Inner-Product-Space v w =
+      equational-reasoning
+        inner-product-ℝ-Inner-Product-Space V (neg-ℝ-Inner-Product-Space V v) w
+        ＝
+          inner-product-ℝ-Inner-Product-Space
+            ( V)
+            ( w)
+            ( neg-ℝ-Inner-Product-Space V v)
+          by symmetric-inner-product-ℝ-Inner-Product-Space V _ _
+        ＝ neg-ℝ (inner-product-ℝ-Inner-Product-Space V w v)
+          by right-negative-law-inner-product-ℝ-Inner-Product-Space w v
+        ＝ neg-ℝ (inner-product-ℝ-Inner-Product-Space V v w)
+          by ap neg-ℝ (symmetric-inner-product-ℝ-Inner-Product-Space V w v)
+```
+
+### The norm of the sum of two vectors
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Inner-Product-Space l1 l2)
+  where
+
+  abstract
+    squared-norm-add-ℝ-Inner-Product-Space :
+      (v w : type-ℝ-Inner-Product-Space V) →
+      squared-norm-ℝ-Inner-Product-Space V (add-ℝ-Inner-Product-Space V v w) ＝
+      ( squared-norm-ℝ-Inner-Product-Space V v +ℝ
+        real-ℕ 2 *ℝ inner-product-ℝ-Inner-Product-Space V v w +ℝ
+        squared-norm-ℝ-Inner-Product-Space V w)
+    squared-norm-add-ℝ-Inner-Product-Space v w =
+      let
+        ⟨_,V_⟩ = inner-product-ℝ-Inner-Product-Space V
+        _+V_ = add-ℝ-Inner-Product-Space V
+      in
+        equational-reasoning
+          ⟨ v +V w ,V v +V w ⟩
+          ＝ ⟨ v ,V v +V w ⟩ +ℝ ⟨ w ,V v +V w ⟩
+            by is-left-additive-inner-product-ℝ-Inner-Product-Space V _ _ _
+          ＝ (⟨ v ,V v ⟩ +ℝ ⟨ v ,V w ⟩) +ℝ (⟨ w ,V v ⟩ +ℝ ⟨ w ,V w ⟩)
+            by
+              ap-add-ℝ
+                ( is-right-additive-inner-product-ℝ-Inner-Product-Space V _ _ _)
+                ( is-right-additive-inner-product-ℝ-Inner-Product-Space V _ _ _)
+          ＝ ⟨ v ,V v ⟩ +ℝ ⟨ v ,V w ⟩ +ℝ ⟨ w ,V v ⟩ +ℝ ⟨ w ,V w ⟩
+            by inv (associative-add-ℝ _ _ _)
+          ＝ ⟨ v ,V v ⟩ +ℝ (⟨ v ,V w ⟩ +ℝ ⟨ w ,V v ⟩) +ℝ ⟨ w ,V w ⟩
+            by ap-add-ℝ (associative-add-ℝ _ _ _) refl
+          ＝ ⟨ v ,V v ⟩ +ℝ (⟨ v ,V w ⟩ +ℝ ⟨ v ,V w ⟩) +ℝ ⟨ w ,V w ⟩
+            by
+              ap-add-ℝ
+                ( ap-add-ℝ
+                  ( refl)
+                  ( ap-add-ℝ
+                    ( refl)
+                    ( symmetric-inner-product-ℝ-Inner-Product-Space V w v)))
+                ( refl)
+          ＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ ⟨ v ,V w ⟩ +ℝ ⟨ w ,V w ⟩
+            by ap-add-ℝ (ap-add-ℝ refl (inv (left-mul-real-ℕ 2 _))) refl
+```
+
+### The real inner product space of the real numbers
+
+```agda
+bilinear-form-mul-ℝ :
+  (l : Level) → bilinear-form-ℝ-Vector-Space (real-vector-space-ℝ l)
+bilinear-form-mul-ℝ l =
+  ( mul-ℝ ,
+    right-distributive-mul-add-ℝ ,
+    associative-mul-ℝ ,
+    left-distributive-mul-add-ℝ ,
+    λ c x y → left-swap-mul-ℝ x c y)
+
+is-inner-product-bilinear-form-mul-ℝ :
+  (l : Level) →
+  is-inner-product-bilinear-form-ℝ-Vector-Space
+    ( real-vector-space-ℝ l)
+    ( bilinear-form-mul-ℝ l)
+is-inner-product-bilinear-form-mul-ℝ l =
+  ( commutative-mul-ℝ ,
+    is-nonnegative-square-ℝ ,
+    eq-zero-eq-zero-square-ℝ)
+
+real-inner-product-space-ℝ : (l : Level) → ℝ-Inner-Product-Space l (lsuc l)
+real-inner-product-space-ℝ l =
+  ( real-vector-space-ℝ l ,
+    bilinear-form-mul-ℝ l ,
+    is-inner-product-bilinear-form-mul-ℝ l)
+```
+
+## External links
+
+- [Inner product space](https://en.wikipedia.org/wiki/Inner_product_space) on
+  Wikipedia
+- [inner product space](https://ncatlab.org/nlab/show/inner+product+space) on
+  $n$Lab
diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md
index bc1d8cd6f2..62eeac6439 100644
--- a/src/linear-algebra/real-vector-spaces.lagda.md
+++ b/src/linear-algebra/real-vector-spaces.lagda.md
@@ -1,17 +1,24 @@
 # Real vector spaces
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module linear-algebra.real-vector-spaces where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
 open import foundation.identity-types
 open import foundation.sets
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import group-theory.abelian-groups
+open import group-theory.multiples-of-elements-abelian-groups
 
 open import linear-algebra.vector-spaces
 
@@ -63,12 +70,23 @@ module _
   zero-ℝ-Vector-Space : type-ℝ-Vector-Space
   zero-ℝ-Vector-Space = zero-Ab ab-ℝ-Vector-Space
 
+  is-zero-prop-ℝ-Vector-Space : subtype l2 type-ℝ-Vector-Space
+  is-zero-prop-ℝ-Vector-Space = is-zero-prop-Ab ab-ℝ-Vector-Space
+
+  is-zero-ℝ-Vector-Space : type-ℝ-Vector-Space → UU l2
+  is-zero-ℝ-Vector-Space = is-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 (heyting-field-ℝ l1) V
 
+  diff-ℝ-Vector-Space :
+    type-ℝ-Vector-Space → type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  diff-ℝ-Vector-Space v w =
+    add-ℝ-Vector-Space v (neg-ℝ-Vector-Space w)
+
   associative-add-ℝ-Vector-Space :
     (v w x : type-ℝ-Vector-Space) →
     add-ℝ-Vector-Space (add-ℝ-Vector-Space v w) x ＝
@@ -100,6 +118,16 @@ module _
     add-ℝ-Vector-Space v w ＝ add-ℝ-Vector-Space w v
   commutative-add-ℝ-Vector-Space = commutative-add-Ab ab-ℝ-Vector-Space
 
+  add-diff-ℝ-Vector-Space :
+    (v w x : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space (diff-ℝ-Vector-Space v w) (diff-ℝ-Vector-Space w x) ＝
+    diff-ℝ-Vector-Space v x
+  add-diff-ℝ-Vector-Space = add-right-subtraction-Ab ab-ℝ-Vector-Space
+
+  neg-neg-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) → neg-ℝ-Vector-Space (neg-ℝ-Vector-Space v) ＝ v
+  neg-neg-ℝ-Vector-Space = neg-neg-Ab ab-ℝ-Vector-Space
+
   left-unit-law-mul-ℝ-Vector-Space :
     (v : type-ℝ-Vector-Space) →
     mul-ℝ-Vector-Space (raise-ℝ l1 one-ℝ) v ＝ v
@@ -158,6 +186,56 @@ module _
     mul-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ neg-ℝ-Vector-Space v
   mul-neg-one-ℝ-Vector-Space =
     mul-neg-one-Vector-Space (heyting-field-ℝ l1) V
+
+  ap-add-ℝ-Vector-Space :
+    {x x' y y' : type-ℝ-Vector-Space} → x ＝ x' → y ＝ y' →
+    add-ℝ-Vector-Space x y ＝ add-ℝ-Vector-Space x' y'
+  ap-add-ℝ-Vector-Space = ap-add-Ab ab-ℝ-Vector-Space
+```
+
+## Properties
+
+### Multiplication by a natural number is iterated addition
+
+```agda
+module _
+  {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    left-mul-real-ℕ-ℝ-Vector-Space :
+      (n : ℕ) (v : type-ℝ-Vector-Space V) →
+      mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ n)) v ＝
+      multiple-Ab (ab-ℝ-Vector-Space V) n v
+    left-mul-real-ℕ-ℝ-Vector-Space 0 v =
+      left-zero-law-mul-ℝ-Vector-Space V v
+    left-mul-real-ℕ-ℝ-Vector-Space 1 v =
+      left-unit-law-mul-ℝ-Vector-Space V v
+    left-mul-real-ℕ-ℝ-Vector-Space (succ-ℕ n@(succ-ℕ _)) v =
+      equational-reasoning
+        mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ (succ-ℕ n))) v
+        ＝ mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ n) +ℝ raise-ℝ l1 one-ℝ) v
+          by
+            ap
+              ( λ c → mul-ℝ-Vector-Space V c v)
+              ( equational-reasoning
+                raise-ℝ l1 (real-ℕ (succ-ℕ n))
+                ＝ raise-ℝ l1 (real-ℕ n +ℝ one-ℝ)
+                  by ap (raise-ℝ l1) (inv (add-real-ℕ n 1))
+                ＝ raise-ℝ l1 (real-ℕ n) +ℝ raise-ℝ l1 one-ℝ
+                  by distributive-raise-add-ℝ l1 (real-ℕ n) one-ℝ)
+        ＝
+          add-ℝ-Vector-Space V
+            ( mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ n)) v)
+            ( mul-ℝ-Vector-Space V (raise-ℝ l1 one-ℝ) v)
+          by right-distributive-mul-add-ℝ-Vector-Space V _ _ _
+        ＝
+          multiple-Ab (ab-ℝ-Vector-Space V) (succ-ℕ n) v
+          by
+            ap-add-ℝ-Vector-Space
+              ( V)
+              ( left-mul-real-ℕ-ℝ-Vector-Space n v)
+              ( left-unit-law-mul-ℝ-Vector-Space V v)
 ```
 
 ### The real numbers are a real vector space
diff --git a/src/linear-algebra/symmetric-bilinear-forms-real-vector-spaces.lagda.md b/src/linear-algebra/symmetric-bilinear-forms-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..d1d7d97c04
--- /dev/null
+++ b/src/linear-algebra/symmetric-bilinear-forms-real-vector-spaces.lagda.md
@@ -0,0 +1,61 @@
+# Symmetric bilinear forms in real vector spaces
+
+```agda
+module linear-algebra.symmetric-bilinear-forms-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import linear-algebra.bilinear-forms-real-vector-spaces
+open import linear-algebra.real-vector-spaces
+
+open import real-numbers.dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+A [bilinear form](linear-algebra.bilinear-forms-real-vector-spaces.md) `B` on a
+[real vector space](linear-algebra.real-vector-spaces.md) `V` is
+{{#concept "symmetric" Agda=is-symmetric-bilinear-form-ℝ-Vector-Space Disambiguation="a bilinear form on a real vector space" WDID=Q2100018 WD="symmetric bilinear form"}}
+if `B u v ＝ B v u` for all `u` and `v` in `V`.
+
+## Definition
+
+### Symmetry of a bilinear form
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Vector-Space l1 l2)
+  (B : bilinear-form-ℝ-Vector-Space V)
+  where
+
+  is-symmetric-prop-bilinear-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-symmetric-prop-bilinear-form-ℝ-Vector-Space =
+    Π-Prop
+      ( type-ℝ-Vector-Space V)
+      ( λ x →
+        Π-Prop
+          ( type-ℝ-Vector-Space V)
+          ( λ y →
+            Id-Prop
+              ( ℝ-Set l1)
+              ( map-bilinear-form-ℝ-Vector-Space V B x y)
+              ( map-bilinear-form-ℝ-Vector-Space V B y x)))
+
+  is-symmetric-bilinear-form-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-symmetric-bilinear-form-ℝ-Vector-Space =
+    type-Prop is-symmetric-prop-bilinear-form-ℝ-Vector-Space
+```
+
+## External links
+
+- [Symmetric bilinear form](https://en.wikipedia.org/wiki/Symmetric_bilinear_form)
+  on Wikipedia
diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
index 204e54f0cd..0595caeeb4 100644
--- a/src/literature/100-theorems.lagda.md
+++ b/src/literature/100-theorems.lagda.md
@@ -31,6 +31,15 @@ open import elementary-number-theory.rational-numbers using
   ( is-countable-ℚ)
 ```
 
+### 4. The Pythagorean Theorem
+
+**Author:** [Louis Wasserman](https://github.com/lowasser)
+
+```agda
+open import linear-algebra.orthogonality-real-inner-product-spaces using
+  ( pythagorean-theorem-ℝ-Inner-Product-Space)
+```
+
 ### 11. The infinitude of primes {#11}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
diff --git a/src/literature/wikipedia-list-of-theorems.lagda.md b/src/literature/wikipedia-list-of-theorems.lagda.md
index 0c7846e7b9..cfb9ff5de7 100644
--- a/src/literature/wikipedia-list-of-theorems.lagda.md
+++ b/src/literature/wikipedia-list-of-theorems.lagda.md
@@ -149,6 +149,15 @@ open import foundation.lawveres-fixed-point-theorem using
   ( fixed-point-theorem-Lawvere)
 ```
 
+### Pythagorean theorem {#Q11518}
+
+**Author:** [Louis Wasserman](https://github.com/lowasser)
+
+```agda
+open import linear-algebra.orthogonality-real-inner-product-spaces using
+  ( pythagorean-theorem-ℝ-Inner-Product-Space)
+```
+
 ### Yoneda lemma {#Q320577}
 
 **Author:** [Emily Riehl](https://emilyriehl.github.io/)
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 26bb420996..9fb6e1249d 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -28,6 +28,7 @@ open import real-numbers.difference-real-numbers public
 open import real-numbers.distance-real-numbers public
 open import real-numbers.enclosing-closed-rational-intervals-real-numbers public
 open import real-numbers.equality-real-numbers public
+open import real-numbers.extensionality-multiplication-bilinear-form-real-numbers public
 open import real-numbers.field-of-real-numbers public
 open import real-numbers.finitely-enumerable-subsets-real-numbers public
 open import real-numbers.geometric-sequences-real-numbers public
diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md
index 6e56c70a08..371e592c16 100644
--- a/src/real-numbers/absolute-value-real-numbers.lagda.md
+++ b/src/real-numbers/absolute-value-real-numbers.lagda.md
@@ -14,6 +14,7 @@ open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.squares-rational-numbers
 
 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.empty-types
@@ -39,6 +40,7 @@ open import real-numbers.negative-real-numbers
 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.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.saturation-inequality-real-numbers
 open import real-numbers.similarity-real-numbers
@@ -90,6 +92,23 @@ abstract opaque
     preserves-sim-max-ℝ _ _ x~x' _ _ (preserves-sim-neg-ℝ x~x')
 ```
 
+### The absolute value commutes with raising the universe level of a real number
+
+```agda
+abstract
+  abs-raise-ℝ :
+    {l1 : Level} (l2 : Level) (x : ℝ l1) →
+    abs-ℝ (raise-ℝ l2 x) ＝ raise-ℝ l2 (abs-ℝ x)
+  abs-raise-ℝ l2 x =
+    eq-sim-ℝ
+      ( similarity-reasoning-ℝ
+        abs-ℝ (raise-ℝ l2 x)
+        ~ℝ abs-ℝ x
+          by preserves-sim-abs-ℝ (sim-raise-ℝ' l2 x)
+        ~ℝ raise-ℝ l2 (abs-ℝ x)
+          by sim-raise-ℝ l2 (abs-ℝ x))
+```
+
 ### The absolute value of a real number is nonnegative
 
 ```agda
@@ -183,6 +202,22 @@ module _
 ### If `|x| ＝ 0` then `x ＝ 0`
 
 ```agda
+module _
+  {l : Level} (x : ℝ l) (|x|~0 : sim-ℝ (abs-ℝ x) zero-ℝ)
+  where
+
+  abstract
+    sim-zero-sim-zero-abs-ℝ : sim-ℝ x zero-ℝ
+    sim-zero-sim-zero-abs-ℝ =
+      sim-sim-leq-ℝ
+        ( transitive-leq-ℝ _ _ _ (leq-sim-ℝ |x|~0) (leq-abs-ℝ x) ,
+          binary-tr
+            ( leq-ℝ)
+            ( neg-zero-ℝ)
+            ( neg-neg-ℝ x)
+            ( neg-leq-ℝ
+              ( transitive-leq-ℝ _ _ _ (leq-sim-ℝ |x|~0) (neg-leq-abs-ℝ x))))
+
 module _
   (x : ℝ lzero) (|x|=0 : abs-ℝ x ＝ zero-ℝ)
   where
@@ -190,14 +225,7 @@ module _
   abstract
     is-zero-is-zero-abs-ℝ : x ＝ zero-ℝ
     is-zero-is-zero-abs-ℝ =
-      antisymmetric-leq-ℝ
-        ( x)
-        ( zero-ℝ)
-        ( tr (leq-ℝ x) |x|=0 (leq-abs-ℝ x))
-        ( tr
-          ( λ y → leq-ℝ y x)
-          ( (ap neg-ℝ |x|=0) ∙ neg-zero-ℝ)
-          ( leq-neg-abs-ℝ x))
+      eq-sim-ℝ (sim-zero-sim-zero-abs-ℝ x (sim-eq-ℝ |x|=0))
 ```
 
 ### If `|x| ≤ 0` then `|x| ＝ 0` and `x ＝ 0`
diff --git a/src/real-numbers/addition-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md
index 8f67041ac9..75828834cb 100644
--- a/src/real-numbers/addition-real-numbers.lagda.md
+++ b/src/real-numbers/addition-real-numbers.lagda.md
@@ -9,8 +9,12 @@ module real-numbers.addition-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-integers
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
@@ -341,6 +345,39 @@ module _
         ( λ z → sim-ℝ z x)
         ( right-swap-add-ℝ x y (neg-ℝ y))
         ( cancel-right-add-diff-ℝ)
+
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where
+
+  abstract
+    cancel-left-conjugation-ℝ : sim-ℝ ((x +ℝ y) +ℝ neg-ℝ x) y
+    cancel-left-conjugation-ℝ =
+      tr
+        ( λ z → sim-ℝ z y)
+        ( ap-add-ℝ (commutative-add-ℝ y x) refl)
+        ( cancel-right-add-diff-ℝ y x)
+
+    cancel-right-conjugation-ℝ : sim-ℝ (x +ℝ (y +ℝ neg-ℝ x)) y
+    cancel-right-conjugation-ℝ =
+      tr
+        ( λ z → sim-ℝ z y)
+        ( commutative-add-ℝ _ _)
+        ( cancel-right-diff-add-ℝ y x)
+
+    cancel-left-add-diff-ℝ : sim-ℝ (x +ℝ (neg-ℝ x +ℝ y)) y
+    cancel-left-add-diff-ℝ =
+      tr
+        ( λ z → sim-ℝ z y)
+        ( ap-add-ℝ refl (commutative-add-ℝ _ _))
+        ( cancel-right-conjugation-ℝ)
+
+    cancel-left-diff-add-ℝ : sim-ℝ (neg-ℝ x +ℝ (x +ℝ y)) y
+    cancel-left-diff-add-ℝ =
+      tr
+        ( λ z → sim-ℝ z y)
+        ( commutative-add-ℝ _ _)
+        ( cancel-left-conjugation-ℝ)
 ```
 
 ### Addition reflects similarity
@@ -385,6 +422,23 @@ module _
   pr2 iff-translate-left-sim-ℝ = reflects-sim-left-add-ℝ z x y
 ```
 
+### Raising the universe level of real numbers distributes over addition
+
+```agda
+abstract
+  distributive-raise-add-ℝ :
+    {l1 l2 : Level} (l3 : Level) (x : ℝ l1) (y : ℝ l2) →
+    raise-ℝ l3 (x +ℝ y) ＝ raise-ℝ l3 x +ℝ raise-ℝ l3 y
+  distributive-raise-add-ℝ l3 x y =
+    eq-sim-ℝ
+      ( similarity-reasoning-ℝ
+        raise-ℝ l3 (x +ℝ y)
+        ~ℝ x +ℝ y
+          by sim-raise-ℝ' l3 (x +ℝ y)
+        ~ℝ raise-ℝ l3 x +ℝ raise-ℝ l3 y
+          by preserves-sim-add-ℝ (sim-raise-ℝ l3 x) (sim-raise-ℝ l3 y))
+```
+
 ### The inclusion of rational numbers preserves addition
 
 ```agda
@@ -427,6 +481,34 @@ abstract
       ＝ x +ℝ real-ℚ (p +ℚ q) by ap (x +ℝ_) (add-real-ℚ p q)
 ```
 
+### The inclusion of integers preserves addition
+
+```agda
+abstract
+  add-real-ℤ : (x y : ℤ) → real-ℤ x +ℝ real-ℤ y ＝ real-ℤ (x +ℤ y)
+  add-real-ℤ x y =
+    equational-reasoning
+      real-ℤ x +ℝ real-ℤ y
+      ＝ real-ℚ (rational-ℤ x +ℚ rational-ℤ y)
+        by add-real-ℚ _ _
+      ＝ real-ℤ (x +ℤ y)
+        by ap real-ℚ (add-rational-ℤ x y)
+```
+
+### The inclusion of natural numbers preserves addition
+
+```agda
+abstract
+  add-real-ℕ : (x y : ℕ) → real-ℕ x +ℝ real-ℕ y ＝ real-ℕ (x +ℕ y)
+  add-real-ℕ x y =
+    equational-reasoning
+      real-ℕ x +ℝ real-ℕ y
+      ＝ real-ℤ (int-ℕ x +ℤ int-ℕ y)
+        by add-real-ℤ _ _
+      ＝ real-ℕ (x +ℕ y)
+        by ap real-ℤ (add-int-ℕ x y)
+```
+
 ### Interchange laws for addition on real numbers
 
 ```agda
diff --git a/src/real-numbers/extensionality-multiplication-bilinear-form-real-numbers.lagda.md b/src/real-numbers/extensionality-multiplication-bilinear-form-real-numbers.lagda.md
new file mode 100644
index 0000000000..1eeb4f0589
--- /dev/null
+++ b/src/real-numbers/extensionality-multiplication-bilinear-form-real-numbers.lagda.md
@@ -0,0 +1,66 @@
+# Extensionality of multiplication of real numbers as a bilinear form
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.extensionality-multiplication-bilinear-form-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.nonnegative-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
+open import real-numbers.square-roots-nonnegative-real-numbers
+open import real-numbers.squares-real-numbers
+```
+
+</details>
+
+## Idea
+
+If the [square](real-numbers.squares-real-numbers.md) of a
+[real number](real-numbers.dedekind-real-numbers.md) is
+[similar](real-numbers.similarity-real-numbers.md) to 0, the real number is
+similar to 0. This property is extensionality of multiplication as a
+[bilinear form](linear-algebra.bilinear-forms-real-vector-spaces.md) over the
+[real vector space of real numbers](linear-algebra.real-vector-spaces.md).
+
+## Proof
+
+```agda
+abstract
+  sim-zero-sim-zero-square-ℝ :
+    {l : Level} (x : ℝ l) → sim-ℝ (square-ℝ x) zero-ℝ → sim-ℝ x zero-ℝ
+  sim-zero-sim-zero-square-ℝ x x²~0 =
+    sim-zero-sim-zero-abs-ℝ
+      ( x)
+      ( inv-tr
+        ( λ y → sim-ℝ y zero-ℝ)
+        ( eq-abs-sqrt-square-ℝ x)
+        ( transitive-sim-ℝ _ _ _
+          ( sim-eq-ℝ real-sqrt-zero-ℝ⁰⁺)
+          ( preserves-sim-sqrt-ℝ⁰⁺
+            ( nonnegative-square-ℝ x)
+            ( zero-ℝ⁰⁺)
+            ( x²~0))))
+
+  eq-zero-eq-zero-square-ℝ :
+    {l : Level} (x : ℝ l) → square-ℝ x ＝ raise-ℝ l zero-ℝ →
+    x ＝ raise-ℝ l zero-ℝ
+  eq-zero-eq-zero-square-ℝ {l} x x²=0 =
+    eq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _
+        ( sim-raise-ℝ l zero-ℝ)
+        ( sim-zero-sim-zero-square-ℝ
+          ( x)
+          ( transitive-sim-ℝ _ _ _ (sim-raise-ℝ' l zero-ℝ) (sim-eq-ℝ x²=0))))
+```
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 117bd2589a..53ff5dac8f 100644
--- a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md
+++ b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md
@@ -686,3 +686,12 @@ is-positive-sqrt-iff-is-positive-ℝ⁰⁺ x =
   ( is-positive-is-positive-sqrt-ℝ⁰⁺ x ,
     is-positive-sqrt-is-positive-ℝ⁰⁺ x)
 ```
+
+### The square root of zero is zero
+
+```agda
+abstract
+  real-sqrt-zero-ℝ⁰⁺ : real-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ ＝ zero-ℝ
+  real-sqrt-zero-ℝ⁰⁺ =
+    inv (eq-sim-ℝ (unique-sqrt-ℝ⁰⁺ zero-ℝ⁰⁺ zero-ℝ⁰⁺ (left-zero-law-mul-ℝ _)))
+```