# mathlibdocumentation

analysis.complex.isometry

# Isometries of the Complex Plane #

The lemma linear_isometry_complex states the classification of isometries in the complex plane. Specifically, isometries with rotations but without translation. The proof involves:

1. creating a linear isometry g with two fixed points, g(0) = 0, g(1) = 1
2. applying linear_isometry_complex_aux to g The proof of linear_isometry_complex_aux is separated in the following parts:
3. show that the real parts match up: linear_isometry.re_apply_eq_re
4. show that I maps to either I or -I
5. every z is a linear combination of a + b * I

## References #

def rotation_aux (a : circle) :

An element of the unit circle defines a linear_isometry_equiv from ℂ to itself, by rotation. This is an auxiliary construction; use rotation, which has more structure, by preference.

Equations
def rotation  :

An element of the unit circle defines a linear_isometry_equiv from ℂ to itself, by rotation.

Equations
@[simp]
theorem rotation_apply (a : circle) (z : ) :
(rotation a) z = (a) * z
theorem linear_isometry_equiv.congr_fun {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [ E] [ F] {f g : E ≃ₗᵢ[R] F} (h : f = g) (x : E) :
f x = g x

Takes an element of ℂ ≃ₗᵢ[ℝ] ℂ and checks if it is a rotation, returns an element of the unit circle.

Equations
@[simp]
theorem rotation_of_rotation (a : circle) :
= a
theorem linear_isometry.re_apply_eq_re_of_add_conj_eq (f : →ₗᵢ[] ) (h₃ : ∀ (z : ), = f z + complex.conj (f z)) (z : ) :
(f z).re = z.re
theorem linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : →ₗᵢ[] } (h₂ : ∀ (z : ), (f z).re = z.re) (z : ) :
(f z).im = z.im (f z).im = -z.im
theorem linear_isometry.re_apply_eq_re {f : →ₗᵢ[] } (h : f 1 = 1) (z : ) :
(f z).re = z.re