Formal Book
1
Six proofs of the infinity of primes
▶
1.1
Appendix: Infinitely many more proofs
2
Bertrand’s postulate
▶
2.1
Appendix: Some estimates
3
Binomial coefficients are (almost) never powers
4
Representing numbers as sums of two squares
5
The law of quadratic reciprocity
6
Every finite division ring is a field
7
The spectral theorem and Hadamard’s determinant problem
8
Some irrational numbers
9
Four times \(π^2/6\)
10
Hilbert’s third problem: decomposing polyhedra
11
Lines in the plane and decompositions of graphs
12
The slope problem
13
Three applications of Euler’s formula
14
Cauchy’s rigidity theorem
15
The Borromean rings don’t exist
16
Touching simplices
17
Every large point set has an obtuse angle
18
Borsuk’s conjecture
19
Sets, functions, and the continuum hypothesis
▶
Appendix: On cardinal and ordinal numbers
20
In praise of inequalities
21
The fundamental theorem of algebra
22
One square and an odd number of triangles
▶
Appendix: Extending valuations
23
A theorem of Pólya on polynomials
▶
23.1
Appendix: Chebyshev’s theorem
24
Van der Waerden’s permanent conjecture
25
On a lemma of Littlewood and Offord
26
Cotangent and the Herglotz trick
27
Buffon’s needle problem
28
Pigeon-hole and double counting
▶
28.1
Numbers
28.2
Sequences
28.3
Sums
28.4
Numbers again
28.5
Graphs
28.6
Sperner’s Lemma
29
Tiling rectangles
30
Three famous theorems on finite sets
31
Shuffling cards
32
Lattice paths and determinants
33
Cayley’s formula for the number of trees
34
Identities versus bijections
35
The finite Kakeya problem
36
Completing Latin squares
37
Permanents and the power of entropy
▶
37.1
Appendix: More about entropy
38
The Dinitz problem
39
Five-coloring plane graphs
40
How to guard a museum
41
Turán’s graph theorem
42
Communicating without errors
43
The chromatic number of Kneser graphs
▶
43.1
Appendix: A proof sketch for the Borsuk–Ulam theorem
44
Of friends and politicians
45
Probability makes counting (sometimes) easy
Dependency graph
6 Every finite division ring is a field
Theorem
6.1
Wedderburn’s theorem
#
L∃∀N
Lean declarations
wedderburn
Every finite division ring is commutative
Proof
▶
TODO