Wikipedia’s list of theorems

Content created by Fredrik Bakke.

Created on 2025-08-30.
Last modified on 2025-08-30.

On this page, we record formalized results in the agda-unimath library that are on Wikipedia’s list of theorems or have a Wikidata entry listed as an instance of a theorem. Additions to this list are very welcome!

module literature.wikipedia-list-of-theorems where

Formalized theorems

The theorems are ordered alphabetically, omitting leading 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)

Recent changes