mathlib

abde2102 - feat(analysis/complex/isometry): restate result more abstractly (#7908)

feat(analysis/complex/isometry): restate result more abstractly (#7908) Define `rotation` as a group homomorphism from the circle to the isometry group of `ℂ`. State the classification of isometries of `ℂ` more abstractly, using this construction. Also golf some proofs.