Formalizing 100 Theorems

Content created by Fredrik Bakke.

Created on 2024-10-17.
Last modified on 2024-10-17.

This file records formalized results from Freek Wiedijk’s Formalizing 100 Theorems. [Wie]

module literature.100-theorems where

The list

3. The Denumerability of the Rational Numbers

open import elementary-number-theory.rational-numbers using
  ( is-countable-ℚ)

11. The Infinitude of Primes

open import elementary-number-theory.infinitude-of-primes using
  ( infinitude-of-primes-ℕ)

22. The Non-Denumerability of the Continuum

This is not yet formalized.

25. Schröder–Bernstein Theorem

open import foundation.cantor-schroder-bernstein-escardo using
  ( Cantor-Schröder-Bernstein)

44. The Binomial Theorem

open import commutative-algebra.binomial-theorem-commutative-semirings using
  ( binomial-theorem-Commutative-Semiring)
open import ring-theory.binomial-theorem-rings using
  ( binomial-theorem-Ring)
open import ring-theory.binomial-theorem-semirings using
  ( binomial-theorem-Semiring)
open import elementary-number-theory.binomial-theorem-integers using
  ( binomial-theorem-ℤ)
open import elementary-number-theory.binomial-theorem-natural-numbers using
  ( binomial-theorem-ℕ)

52. The Number of Subsets of a Set

This is not yet formalized.

63. Cantor’s Theorem

open import foundation.cantors-theorem using
  ( theorem-Cantor)

69. Greatest Common Divisor Algorithm

open import
  elementary-number-theory.greatest-common-divisor-natural-numbers using
  ( GCD-ℕ)

74. The Principle of Mathematical Induction

open import elementary-number-theory.natural-numbers using
  ( ind-ℕ)

80. The Fundamental Theorem of Arithmetic

open import elementary-number-theory.fundamental-theorem-of-arithmetic using
  ( fundamental-theorem-arithmetic-list-ℕ)

91. The Triangle Inequality

open import real-numbers.metric-space-of-real-numbers using
  ( is-triangular-premetric-leq-ℝ)

96. Principle of Inclusion/Exclusion

This is not yet formalized.

References

[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.
  • The spiritual successor to Formalizing 100 Theorems is 1000+ theorems, also due to Freek Wiedijk.

Recent changes