English
For a complex-linear real isometry f with f 1 = 1, f is either a rotation by some a or equals conjLIE composed with a rotation by some a.
Русский
Для линейной изометрии f на ℂ, удовлетворяющей f 1 = 1, либо f есть вращение на некотором a, либо f = conjLIE ⋅ rotation a.
LaTeX
$$$\forall {f : ℂ \toℓᵢ[ℝ] ℂ}, f 1 = 1 \Rightarrow (\exists a, f = rotation a) \lor (\exists a, f = conjLIE.trans (rotation a))$$$
Lean4
theorem linear_isometry_complex_aux {f : ℂ ≃ₗᵢ[ℝ] ℂ} (h : f 1 = 1) : f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE :=
by
have h0 : f I = I ∨ f I = -I :=
by
simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
constructor
· rw [← I_re]
exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
· apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
intro z
rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]
refine h0.imp (fun h' : f I = I => ?_) fun h' : f I = -I => ?_ <;>
· apply LinearIsometryEquiv.toLinearEquiv_injective
apply Complex.basisOneI.ext'
intro i
fin_cases i <;> simp [h, h']