Formula for the number of combinations (#1213)

I must have misremembered when I thought we didn't do the formula of
combinations yet. It seems to be in the library already, although it can
definitely be formalized more clearly (this is old stuff that predates
agda-unimath).

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}}