Commit 2021-07-09 12:52 abde2102

View on Github →

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.

Estimated changes

Modified src/analysis/complex/isometry.lean

deleted theorem linear_isometry.abs_apply_sub_one_eq_abs_sub_one

modified theorem linear_isometry_complex

modified theorem linear_isometry_complex_aux

added def rotation

added theorem rotation_apply

added def rotation_aux

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry_equiv.coe_to_continuous_linear_equiv

added def linear_isometry_equiv.to_continuous_linear_equiv