English
Every real-linear isometry of ℂ is either a rotation by some unit-circle element a or the composition of conjLIE with a rotation by some a.
Русский
Каждая вещественно-линейная изометрия ℂ либо вращение на элементе единичной окружности a, либо композиция conjLIE и вращения на a.
LaTeX
$$$\forall f : \mathbb{C} \simeq\mathbb{C}, \exists a \in \mathbb{C}_{1},\; f = rotation\; a \lor f = conjLIE.trans (rotation\; a)$$$
Lean4
theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ] ℂ) : ∃ a : Circle, f = rotation a ∨ f = conjLIE.trans (rotation a) :=
by
let a : Circle := ⟨f 1, by simp [Submonoid.unitSphere, f.norm_map]⟩
use a
have : (f.trans (rotation a).symm) 1 = 1 := by simpa [a] using rotation_apply a⁻¹ (f 1)
refine (linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_
· simpa using eq_mul_of_inv_mul_eq h₁
· exact eq_mul_of_inv_mul_eq h₂
