mathlib documentation


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 #

noncomputable def rotation  :

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

theorem rotation_apply (a : circle) (z : ) :
theorem rotation_trans (a b : circle) :
noncomputable def rotation_of (e : ≃ₗᵢ[] ) :

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

theorem linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : →ₗᵢ[] } (h₂ : ∀ (z : ), (f z).re = (z : ) :
(f z).im = (f z).im =
theorem linear_isometry.re_apply_eq_re {f : →ₗᵢ[] } (h : f 1 = 1) (z : ) :
(f z).re =

The matrix representation of rotation a is equal to the conformal matrix !![re a, -im a; im a, re a].


The determinant of rotation (as a linear map) is equal to 1.


The determinant of rotation (as a linear equiv) is equal to 1.