Register two Wikipedia theorems (#1709)

Author: fredrik-bakke

src/group-theory/quotient-groups.lagda.md

@@ -42,13 +42,15 @@ 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" 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 **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" 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
@@ -60,6 +62,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`.
 
+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**.
+
 ## Definitions
 
 ### The universal property of quotient groups
@@ -529,7 +536,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 +721,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

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-ℝ)
+```
+
 ### Pythagorean theorem {#Q11518}
 
 **Author:** [Louis Wasserman](https://github.com/lowasser)