Closed as not planned
Description
Properly participating in the 1000+ theorems has a couple of blockers on their side:
- Add support for the Agda proof assistant 1000-plus/1000-plus.github.io#22
- Clarify library classification 1000-plus/1000-plus.github.io#23
- Add stable hyperlinkable anchors to rows 1000-plus/1000-plus.github.io#24
This issue is a branch-out from #1214.
Formalized theorems
- Bezout's lemma, by Bryan Lu
- Binomial theorem, by Egbert Rijke
- Cantor–Schröder–Bernstein theorem, by Elif Uskuplu
- Cantor's theorem, by Egbert Rijke
- Cayley's theorem
- Diaconescu's theorem, by Fredrik Bakke Logic #1226
- Euclid's theorem, by Egbert Rijke
- Fundamental theorem of arithmetic, by Victor Blanchi
- Fundamental theorem of equivalence relations, by Egbert Rijke
- Kleene's fixed point theorem, by Fredrik Bakke
- Knaster–Tarski fixed point theorem, by Fredrik Bakke
- Lawvere's fixed point theorem
- Nicomachus's theorem, by Egbert Rijke Refactor elementary number theory #1211
- Yoneda lemma, by Emily Riehl
Useful links
- 1000-plus.github.io
- 1000-plus/1000-plus.github.io on GitHub
- List of theorems on Wikipedia