From 9dc904028589f42f50421a7fcef9f69b4f8a8d0e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 13 Nov 2025 18:33:16 +0100
Subject: [PATCH 1/4] add two wikipedia theorems

---
 src/group-theory/quotient-groups.lagda.md     | 25 ++++++++++++-----
 .../wikipedia-list-of-theorems.lagda.md       | 27 +++++++++++++++++++
 2 files changed, 45 insertions(+), 7 deletions(-)

diff --git a/src/group-theory/quotient-groups.lagda.md b/src/group-theory/quotient-groups.lagda.md
index d109a8292d..fe625fa0be 100644
--- a/src/group-theory/quotient-groups.lagda.md
+++ b/src/group-theory/quotient-groups.lagda.md
@@ -42,13 +42,14 @@ open import group-theory.semigroups
 ## Idea
 
 Given a [normal subgroup](group-theory.normal-subgroups.md) `N` of `G`, the
-**quotient group** `G/N` is a [group](group-theory.groups.md) equipped with a
+{{#concept "quotient group" Agda=quotient-Group}} `G/N` is a
+[group](group-theory.groups.md) equipped with a
 [group homomorphism](group-theory.homomorphisms-groups.md) `q : G → G/N` such
-that `N ⊆ ker q`, and such that `q` satisfies the **universal property of the
-quotient group**, which asserts that any group homomorphism `f : G → H` such
-that `N ⊆ ker f` extends uniquely along `q` to a group homomorphism `G/N → H`.
-In other words, the universal property of the quotient group `G/N` asserts that
-the map
+that `N ⊆ ker q`, and such that `q` satisfies the
+{{#concept "universal property of the
+quotient group"}}, which asserts that any group homomorphism `f : G → H` such that
+`N ⊆ ker f` extends uniquely along `q` to a group homomorphism `G/N → H`. In other
+words, the universal property of the quotient group `G/N` asserts that the map
 
 ```text
   hom-Group G/N H → nullifying-hom-Group G H N
@@ -60,6 +61,11 @@ from group homomorphisms `G/N → H` to
 group homomorphism is said to be `N`-nullifying if `N` is contained in the
 [kernel](group-theory.kernels-homomorphisms-groups.md) of `f`.
 
+That the quotient group satisfies its universal property is also referred to as
+the
+{{#concept "fundamental theorem on homomorphisms" Disambiguation="of groups" WD="fundamental theorem on homomorphisms" WDID=Q1187646 Agda=is-quotient-group-quotient-Group}},
+or **first isomorphism theorem**.
+
 ## Definitions
 
 ### The universal property of quotient groups
@@ -529,7 +535,7 @@ above. The first map is an equivalence by the universal property of set
 quotients, by which we have:
 
 ```text
-  (G/N → H) ≃ reflecting-map G H.
+  (G/N → H) ≃ reflecting-map G H. ∎
 ```
 
 ```agda
@@ -714,3 +720,8 @@ module _
       unit-congruence-Normal-Subgroup G N
         ( apply-effectiveness-map-quotient-hom-Group G N (inv H))
 ```
+
+## External links
+
+- [Fundamental theorem on homomorphisms](https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms)
+  on Wikipedia
diff --git a/src/literature/wikipedia-list-of-theorems.lagda.md b/src/literature/wikipedia-list-of-theorems.lagda.md
index 0c7846e7b9..dc8e38fc30 100644
--- a/src/literature/wikipedia-list-of-theorems.lagda.md
+++ b/src/literature/wikipedia-list-of-theorems.lagda.md
@@ -117,6 +117,15 @@ open import foundation.fundamental-theorem-of-equivalence-relations using
   ( equiv-equivalence-relation-partition)
 ```
 
+### Fundamental theorem on homomorphisms {#Q1187646}
+
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
+
+```agda
+open import group-theory.quotient-groups using
+  ( is-quotient-group-quotient-Group)
+```
+
 ### Kleene's fixed point theorem {#Q3527263}
 
 **Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke)
@@ -149,6 +158,24 @@ open import foundation.lawveres-fixed-point-theorem using
   ( fixed-point-theorem-Lawvere)
 ```
 
+### Triangle inequality theorem {#Q208216}
+
+**Author:** [malarbol](https://github.com/malarbol)
+
+```agda
+open import real-numbers.metric-space-of-real-numbers using
+  ( is-triangular-neighborhood-ℝ)
+```
+
+**Author:** [Louis Wasserman](https://github.com/lowasser)
+
+```agda
+open import real-numbers.absolute-value-real-numbers using
+  ( triangle-inequality-abs-ℝ)
+open import real-numbers.distance-real-numbers using
+  ( triangle-inequality-dist-ℝ)
+```
+
 ### Yoneda lemma {#Q320577}
 
 **Author:** [Emily Riehl](https://emilyriehl.github.io/)

From e1532d2c1211277f4a2ad90c9765abd89bb16226 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 13 Nov 2025 18:36:05 +0100
Subject: [PATCH 2/4] fix concept

---
 src/group-theory/quotient-groups.lagda.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/group-theory/quotient-groups.lagda.md b/src/group-theory/quotient-groups.lagda.md
index fe625fa0be..3a592690a2 100644
--- a/src/group-theory/quotient-groups.lagda.md
+++ b/src/group-theory/quotient-groups.lagda.md
@@ -42,14 +42,14 @@ open import group-theory.semigroups
 ## Idea
 
 Given a [normal subgroup](group-theory.normal-subgroups.md) `N` of `G`, the
-{{#concept "quotient group" Agda=quotient-Group}} `G/N` is a
-[group](group-theory.groups.md) equipped with a
+{{#concept "quotient group" WD="quotient group" WDID=Q1138961 Agda=quotient-Group}}
+`G/N` is a [group](group-theory.groups.md) equipped with a
 [group homomorphism](group-theory.homomorphisms-groups.md) `q : G → G/N` such
 that `N ⊆ ker q`, and such that `q` satisfies the
-{{#concept "universal property of the
-quotient group"}}, which asserts that any group homomorphism `f : G → H` such that
-`N ⊆ ker f` extends uniquely along `q` to a group homomorphism `G/N → H`. In other
-words, the universal property of the quotient group `G/N` asserts that the map
+{{#concept "universal property of the quotient group" Agda=universal-property-quotient-Group}},
+which asserts that any group homomorphism `f : G → H` such that `N ⊆ ker f`
+extends uniquely along `q` to a group homomorphism `G/N → H`. In other words,
+the universal property of the quotient group `G/N` asserts that the map
 
 ```text
   hom-Group G/N H → nullifying-hom-Group G H N

From c840214aebf0afd9876dc7a74aebe83833e64d43 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 22:59:20 +0000
Subject: [PATCH 3/4] Update quotient-groups.lagda.md

---
 src/group-theory/quotient-groups.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/group-theory/quotient-groups.lagda.md b/src/group-theory/quotient-groups.lagda.md
index 3a592690a2..1638827bf7 100644
--- a/src/group-theory/quotient-groups.lagda.md
+++ b/src/group-theory/quotient-groups.lagda.md
@@ -61,8 +61,8 @@ from group homomorphisms `G/N → H` to
 group homomorphism is said to be `N`-nullifying if `N` is contained in the
 [kernel](group-theory.kernels-homomorphisms-groups.md) of `f`.
 
-That the quotient group satisfies its universal property is also referred to as
-the
+The fact that the quotient group satisfies its universal property is commonly
+known as the
 {{#concept "fundamental theorem on homomorphisms" Disambiguation="of groups" WD="fundamental theorem on homomorphisms" WDID=Q1187646 Agda=is-quotient-group-quotient-Group}},
 or **first isomorphism theorem**.
 

From 5cd5026e93ef517580afd82f5df1883c3c4b3e67 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 23:00:30 +0000
Subject: [PATCH 4/4] Update explanation of universal property in quotient
 groups

Clarify the description of the universal property of quotient groups.
---
 src/group-theory/quotient-groups.lagda.md | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/group-theory/quotient-groups.lagda.md b/src/group-theory/quotient-groups.lagda.md
index 1638827bf7..f0f831a549 100644
--- a/src/group-theory/quotient-groups.lagda.md
+++ b/src/group-theory/quotient-groups.lagda.md
@@ -46,10 +46,11 @@ Given a [normal subgroup](group-theory.normal-subgroups.md) `N` of `G`, the
 `G/N` is a [group](group-theory.groups.md) equipped with a
 [group homomorphism](group-theory.homomorphisms-groups.md) `q : G → G/N` such
 that `N ⊆ ker q`, and such that `q` satisfies the
-{{#concept "universal property of the quotient group" Agda=universal-property-quotient-Group}},
-which asserts that any group homomorphism `f : G → H` such that `N ⊆ ker f`
-extends uniquely along `q` to a group homomorphism `G/N → H`. In other words,
-the universal property of the quotient group `G/N` asserts that the map
+{{#concept "universal property" Disambiguation="of the quotient group" Agda=universal-property-quotient-Group}}
+of the quotient group, which asserts that any group homomorphism `f : G → H`
+such that `N ⊆ ker f` extends uniquely along `q` to a group homomorphism
+`G/N → H`. In other words, the universal property of the quotient group `G/N`
+asserts that the map
 
 ```text
   hom-Group G/N H → nullifying-hom-Group G H N