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/.
External links
- The spiritual successor to Formalizing 100 Theorems is 1000+ theorems, also due to Freek Wiedijk.
Recent changes
- 2024-10-17. Fredrik Bakke. 100 Theorems (#1201).