Isometries of the Complex Plane #
linear_isometry_complex states the classification of isometries in the complex plane.
Specifically, isometries with rotations but without translation.
The proof involves:
- creating a linear isometry
gwith two fixed points,
g(0) = 0,
g(1) = 1
gThe proof of
linear_isometry_complex_auxis separated in the following parts:
- show that the real parts match up:
- show that I maps to either I or -I
- every z is a linear combination of a + b * I