linear_isometry_complex_aux — Mathlib

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']

Похожие утверждения