1000+ theorems

Content created by Fredrik Bakke.

Created on 2025-02-14.
Last modified on 2025-02-14.

On this page, we record formalized results in the agda-unimath library following Freek Wiedijk and collaborators’ 1000+ theorems project [Wie]. This project records the formalization status of theorems in mathematics that have their own Wikipedia entry. We welcome any contribution to this list!

module literature.1000plus-theorems where

Formalized theorems

The theorems are ordered alphabetically, omitting definite articles (“the”).

Bézout’s lemma

Author: Bryan Lu

open import elementary-number-theory.bezouts-lemma-integers using
  ( bezouts-lemma-ℤ)
open import elementary-number-theory.bezouts-lemma-natural-numbers using
  ( bezouts-lemma-ℕ)

Binomial theorem

Author: Egbert Rijke

open import commutative-algebra.binomial-theorem-commutative-rings using
  ( binomial-theorem-Commutative-Ring)
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-ℕ)

Cantor–Schröder–Bernstein theorem

Author: Elif Uskuplu

Note: The formalization of the Cantor-Schröder-Bernstein theorem in agda-unimath is a generalization of the statement to all types, i.e., it is not restricted to sets. This generalization is originally due to Martin-Escardó, hence we refer to the generalization as the Cantor-Schröder-Bernstein-Escardó theorem.

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

Cantor’s theorem

Author: Egbert Rijke

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

Cayley’s theorem

Author: Egbert Rijke

open import group-theory.cayleys-theorem using
  ( Cayleys-theorem)

Diaconescu’s theorem

Author: Fredrik Bakke

open import foundation.diaconescus-theorem using
  ( theorem-Diaconescu)

Euclid’s theorem

Author: Egbert Rijke

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

Fundamental theorem of arithmetic

Author: Victor Blanchi

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

Fundamental theorem of equivalence relations

Author: Egbert Rijke

open import foundation.fundamental-theorem-of-equivalence-relations using
  ( equiv-equivalence-relation-partition)

Kleene’s fixed point theorem

Author: Fredrik Bakke

open import domain-theory.kleenes-fixed-point-theorem-posets using
  ( is-least-fixed-point-theorem-kleene-hom-Poset ;
    is-least-fixed-point-theorem-kleene-Poset)
open import domain-theory.kleenes-fixed-point-theorem-omega-complete-posets using
  ( is-least-fixed-point-theorem-kleene-hom-ω-Complete-Poset ;
    is-least-fixed-point-theorem-kleene-ω-Complete-Poset)

Knaster–Tarski fixed point theorem

Author: Fredrik Bakke

open import order-theory.knaster-tarski-fixed-point-theorem using
  ( least-fixed-point-knaster-tarski-Inflattice ;
    greatest-fixed-point-knaster-tarski-Suplattice)

Lawvere’s fixed point theorem

Author: Egbert Rijke

open import foundation.lawveres-fixed-point-theorem using
  ( fixed-point-theorem-Lawvere)

Yoneda lemma

Author: Emily Riehl

open import category-theory.yoneda-lemma-categories using
  ( lemma-yoneda-Category)
open import category-theory.yoneda-lemma-precategories using
  ( lemma-yoneda-Precategory)

See also

References

[Wiea]
Freek Wiedijk. 1000+ theorems. URL: https://1000-plus.github.io/.
[Wieb]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes