A Blueprint for Short Surreal Numbers in Lean
1
Overview
2
Games, order, and surreal representatives
▶
2.1
Finite games and birthdays
2.2
The recursive order
2.3
Surreal games
3
Addition, negation, and surreal numbers
▶
3.1
Addition and Negation on games
3.2
Surreal Number
4
Multiplication and the Conway induction
▶
4.1
The recursive product
4.2
A simultaneous well-founded proof
4.3
Congruence and associativity
5
The quotient ring and its order
▼
5.1
Multiplication on equivalence classes
5.2
Positive products and ordered-ring compatibility
Dependency graph
5 The quotient ring and its order
5.1
Multiplication on equivalence classes
5.2
Positive products and ordered-ring compatibility