1. Chapter 0 Complex Number Game🔗

Similar to the Natural Number Game, we rewrite the complex number game with rationl numbers as the real and imaginary parts.

Mathematically, the structure implemented is ℚ[i]. The real part and the imaginary parts are rational numbers. So that the examples can be print out more conveniently. Indeed, all calculations by hand in practice is carried out in ℚ[i] instead of ℂ.

In this beginning section, we do not use any functions and theorems from the Real library or the Complex library in Mathlib. All definition in this section are computable.

import Mathlib.Tactic

1. 1.1. Construction
2. 1.2. Arithemtic operations
3. 1.3. Coercion
4. 1.4. Scalar multiplication
5. 1.5. Additive group structure
6. 1.6. Ring structure
7. 1.7. Involution
8. 1.8. Norm square function
9. 1.9. Inversion
10. 1.10. Cast lemmas
11. 1.11. Field
12. 1.12. Geometric applications