add external links and wd identifiers

UniMath · Dec 6, 2023 · 025bc6f · 025bc6f
1 parent b199ab5
commit 025bc6f
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 6 deletions.
diff --git a/src/elementary-number-theory/hardy-ramanujan-number.lagda.md b/src/elementary-number-theory/hardy-ramanujan-number.lagda.md
@@ -20,11 +20,12 @@ open import foundation.unit-type
 
 ## Idea
 
-The {{#concept "Hardy-Ramanujan number"}} is the number `1729`. This number is
-the second [taxicab number](elementary-number-theory.taxicab-numbers.md), i.e.,
-it is the least natural number that can be written as a sum of cubes of positive
-natural numbers in exactly two distinct ways. Specifically, we have the
-identifications
+The
+{{#concept "Hardy-Ramanujan number" Agda=Hardy-Ramanujan-ℕ WD="1729" WDID=Q825176}}
+is the number `1729`. This number is the second
+[taxicab number](elementary-number-theory.taxicab-numbers.md), i.e., it is the
+least natural number that can be written as a sum of cubes of positive natural
+numbers in exactly two distinct ways. Specifically, we have the identifications
 
 ```text
   1³ + 12³ ＝ 1729    and    9³ + 10³ ＝ 1729.
@@ -66,3 +67,7 @@ pr1 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
 pr2 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
   refl
 ```
+
+## External links
+
+- [1729 (number)](<https://en.wikipedia.org/wiki/1729_(number)>) at Wikipedia
diff --git a/src/elementary-number-theory/taxicab-numbers.lagda.md b/src/elementary-number-theory/taxicab-numbers.lagda.md
@@ -26,7 +26,9 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The `n`-th {{#concept "taxicab number"}} `taxicab n` is the smallest
+The `n`-th
+{{#concept "taxicab number" Agda=is-taxicab-number-ℕ WD="taxicab number" WDID=Q1462591}}
+`taxicab n` is the smallest
 [natural number](elementary-number-theory.natural-numbers.md) `x` such that `x`
 is a [sum](elementary-number-theory.addition-natural-numbers.md) of two
 [cubes](elementary-number-theory.cubes-natural-numbers.md) in `n`
@@ -95,3 +97,8 @@ is-taxicab-number-ℕ n x =
 ## See also
 
 - [The Hardy-Ramanujan number](elementary-number-theory.hardy-ramanujan-number.md)
+
+## External links
+
+- [Taxicab numbers](https://en.wikipedia.org/wiki/Taxicab_number) at Wikipedia
+- [Taxicab nubmers](https://oeis.org/A011541) at the OEIS.