Formula for the number of combinations

src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md

@@ -39,6 +39,9 @@ The **binomial theorem** in commutative rings asserts that for any two elements
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
+The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Binomial sums
@@ -174,3 +177,7 @@ is-linear-combination-power-add-Commutative-Ring A =
   is-linear-combination-power-add-Commutative-Semiring
     ( commutative-semiring-Commutative-Ring A)
 ```
+
+## References
+
+{{#bibliography}}

src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md

@@ -39,6 +39,9 @@ we have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
+The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Binomial sums
@@ -185,3 +188,7 @@ is-linear-combination-power-add-Commutative-Semiring A n m x y =
     ( y)
     ( commutative-mul-Commutative-Semiring A x y)
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/bezouts-lemma-integers.lagda.md

@@ -38,6 +38,10 @@ open import foundation.unit-type
 
 </details>
 
+Bézout's Lemma is the 60th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
+originally added to agda-unimath by [Brian Lu](https://blu-bird.github.io).
+
 ## Lemma
 
 ```agda
@@ -532,3 +536,7 @@ div-right-factor-coprime-ℕ x y z H K =
         ( tr (div-ℤ (int-ℕ x)) (inv (mul-int-ℕ y z)) (div-int-div-ℕ H))
       ( eq-gcd-gcd-int-ℕ x y ∙ ap int-ℕ K))
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md

@@ -61,6 +61,10 @@ predicate `P : ℕ → UU lzero` given by
 is decidable, because `P z ⇔ [y]_x | [z]_x` in `ℤ/x`. The least positive `z`
 such that `P z` holds is `gcd x y`.
 
+Bézout's Lemma is the 60th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
+originally added to agda-unimath by [Brian Lu](https://blu-bird.github.io).
+
 ## Definitions
 
 ```agda
@@ -1944,3 +1948,7 @@ bezouts-lemma-eqn-ℕ :
 bezouts-lemma-eqn-ℕ x y H =
   minimal-positive-distance-eqn x y H ∙ bezouts-lemma-ℕ x y H
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/binomial-theorem-integers.lagda.md

@@ -36,6 +36,9 @@ The binomial theorem for the integers asserts that for any two integers `x` and
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
+The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Binomial sums
@@ -103,3 +106,7 @@ binomial-theorem-ℤ :
         ( power-ℤ (dist-ℕ (nat-Fin (succ-ℕ n) i) n) y))
 binomial-theorem-ℤ = binomial-theorem-Commutative-Ring ℤ-Commutative-Ring
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md

@@ -35,6 +35,9 @@ numbers `x` and `y` and any natural number `n`, we have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
+The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Binomial sums
@@ -103,3 +106,7 @@ binomial-theorem-ℕ :
 binomial-theorem-ℕ =
   binomial-theorem-Commutative-Semiring ℕ-Commutative-Semiring
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md

@@ -75,6 +75,9 @@ in several ways:
 Note that the [univalence axiom](foundation-core.univalence.md) is neccessary to
 prove the second uniqueness property of prime factorizations.
 
+The fundamental theorem of arithmetic is the 80th theorem on Freek Wiedijk's
+list of [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Prime decomposition of a natural number with lists
@@ -1092,3 +1095,7 @@ pr2 (prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq) =
 
 - [Fundamental theorem of arithmetic](https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic)
   at Wikipedia
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md

@@ -42,6 +42,10 @@ The greatest common divisor of two natural numbers `x` and `y` is a number
 `gcd x y` such that any natural number `d : ℕ` is a common divisor of `x` and
 `y` if and only if it is a divisor of `gcd x y`.
 
+The algorithm defining the greatest common divisor is the 69th theorem on Freek
+Wiedijk's list of [100 theorems](literature.100-theorems.md)
+{{#cite 100theorems}}.
+
 ## Definition
 
 ### Common divisors
@@ -477,3 +481,7 @@ is-gcd-quotient-div-gcd-ℕ {a} {b} {d} nz H x =
         ( simplify-div-quotient-div-ℕ nz
           ( div-gcd-is-common-divisor-ℕ a b d H))
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/infinitude-of-primes.lagda.md

@@ -44,6 +44,9 @@ that there are infinitely many
 function that returns for each `n` the `n`-th prime, and we obtain the function
 that counts the number of primes below a number `n`.
 
+The infinitude of primes is the 11th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definition
 
 We begin by stating the
@@ -180,3 +183,7 @@ prime-counting-ℕ (succ-ℕ n) =
     ( is-decidable-is-prime-ℕ (succ-ℕ n))
     ( prime-counting-ℕ n)
 ```
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/natural-numbers.lagda.md

@@ -83,6 +83,10 @@ is-not-one-ℕ' n = ¬ (is-one-ℕ' n)
 
 ### The induction principle of ℕ
 
+The induction principle of the natural numbers is the 74th theorem on Freek
+Wiedijk's list of [100 theorems](literature.100-theorems.md)
+{{#cite 100theorems}}.
+
 ```agda
 ind-ℕ :
   {l : Level} {P : ℕ → UU l} →
@@ -147,3 +151,7 @@ is-not-one-two-ℕ ()
   [`strong-induction-natural-numbers`](elementary-number-theory.strong-induction-natural-numbers.md).
 - The based strong induction principle is defined in
   [`based-strong-induction-natural-numbers`](elementary-number-theory.based-strong-induction-natural-numbers.md).
+
+## References
+
+{{#bibliography}}

src/elementary-number-theory/rational-numbers.lagda.md

@@ -39,8 +39,24 @@ open import set-theory.countable-sets
 
 ## Idea
 
-The type of rational numbers is the quotient of the type of fractions, by the
-equivalence relation given by `(n/m) ~ (n'/m') := Id (n *ℤ m') (n' *ℤ m)`.
+The type of
+{{#concept "rational numbers" Agda=ℚ WD="rational number" WDID=Q1244890}} is the
+[quotient](foundation.set-quotients.md) of the type of
+[integer fractions](elementary-number-theory.integer-fractions.md) by the
+[equivalence relation](foundation.equivalence-relations.md) given by
+
+$$
+\frac{n}{m} \sim \frac{n'}{m'} := nm' = n'm.
+$$
+
+Since the
+[reduced fractions](elementary-number-theory.reduced-integer-fractions.md) are
+[canonical representatives](foundation.choice-of-representatives-equivalence-relation.md)
+of the similarity relation on fractions, we simply define the
+[set](foundation.sets.md) `ℚ` to be the type of reduced fractions and we obtain
+the
+[universal property of the set quotient](foundation.universal-property-set-quotients.md)
+from the fact that each equivalence class has a unique canonical representative.
 
 ## Definitions
 
@@ -189,6 +205,10 @@ retract-integer-fraction-ℚ =
 
 ### The rationals are countable
 
+The denumerability of the rational numbers is the third theorem on Freek
+Wiedijk's list of [100 theorems](literature.100-theorems.md)
+{{#cite 100theorems}}.
+
 ```agda
 is-countable-ℚ : is-countable ℚ-Set
 is-countable-ℚ =
@@ -288,3 +308,7 @@ reflecting-map-sim-fraction :
 pr1 reflecting-map-sim-fraction = rational-fraction-ℤ
 pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fraction-ℤ x y H
 ```
+
+## References
+
+{{#bibliography}}

src/foundation/cantor-schroder-bernstein-escardo.lagda.md

@@ -38,6 +38,9 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for
 [embed](foundation-core.embeddings.md) into each other, then the types are
 [equivalent](foundation-core.equivalences.md). {{#cite Esc21}}
 
+The Cantor–Schröder–Bernstein theorem is the 25th theorem on Freek Wiedijk's
+list of [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Statement
 
 ```agda

src/foundation/cantors-theorem.lagda.md

@@ -57,6 +57,9 @@ would have to be a fixed point of the negation operation, since
 
 but negation has no fixed points.
 
+Cantor's theorem is the 63rd theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ```agda
 module _
   {l1 l2 : Level} {X : UU l1} (f : X → powerset l2 X)

src/literature/100-theorems.lagda.md

@@ -42,6 +42,8 @@ sets. This generalization is originally due to Martin-Escardó, hence we refer t
 the generalization as the Cantor-Schröder-Bernstein-Escardó theorem.
 
 ```agda
+open import foundation.cantor-schroder-bernstein-escardo using
+  ( Cantor-Schröder-Bernstein-Escardó)
 open import foundation.cantor-schroder-bernstein-escardo using
   ( Cantor-Schröder-Bernstein)
 ```
@@ -74,6 +76,15 @@ open import univalent-combinatorics.decidable-subtypes using
   ( number-of-elements-decidable-subtype-is-finite)
 ```
 
+### [58. Formula for the number of combinations](https://www.cs.ru.nl/~freek/100/#58) {#58}
+
+Author: Egbert Rijke
+
+```agda
+open import univalent-combinatorics.binomial-types using
+  ( has-cardinality-binomial-type)
+```
+
 ### [60. Bezout's Lemma](https://www.cs.ru.nl/~freek/100/#60) {#60}
 
 Author: Brian Lu

src/real-numbers/metric-space-of-real-numbers.lagda.md

@@ -98,6 +98,9 @@ premetric-leq-ℝ l d x y =
 
 ### The standard premetric on the real numbers is a metric structure
 
+The triangle inequality is the 91st theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ```agda
 is-reflexive-premetric-leq-ℝ :
   {l : Level} → is-reflexive-Premetric (premetric-leq-ℝ l)
@@ -258,3 +261,7 @@ is-isometry-metric-space-leq-real-ℚ d x y =
       ( leq-add-positive-le-le-add-positive-ℚ x y d)
       ( leq-add-positive-le-le-add-positive-ℚ y x d))
 ```
+
+## References
+
+{{#bibliography}}

src/ring-theory/binomial-theorem-rings.lagda.md

@@ -38,6 +38,9 @@ have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
+The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Binomial sums
@@ -157,3 +160,7 @@ is-linear-combination-power-add-Ring :
 is-linear-combination-power-add-Ring R =
   is-linear-combination-power-add-Semiring (semiring-Ring R)
 ```
+
+## References
+
+{{#bibliography}}

src/ring-theory/binomial-theorem-semirings.lagda.md

@@ -41,6 +41,9 @@ have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
+The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
 ## Definitions
 
 ### Binomial sums
@@ -786,3 +789,7 @@ is-linear-combination-power-add-Semiring R n m x y H =
                       ( dist-ℕ (nat-Fin (succ-ℕ m) i) m)
                       ( y))))))))))
 ```
+
+## References
+
+{{#bibliography}}