rightAngleRotation_map_complex — Mathlib

English

The 90-degree rotation J on a 2D oriented real inner product space corresponds, under the complex-number representation f, to multiplication by i: f(Jx) = i f(x) for all x ∈ E.

Русский

Поворот на 90° J в ориентированном двумерном вещественном пространстве в комплексной записи через отображение f соответствует умножению на i: f(Jx) = i f(x).

LaTeX

$$$ f(Jx) = i\, f(x) $$$

Lean4

/-- The rotation by 90 degrees on an oriented real inner product space of dimension 2 can be
evaluated in terms of a complex-number representation of the space. -/
theorem rightAngleRotation_map_complex (f : E ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x : E) : f (J x) = I * f x := by
  rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map, LinearIsometryEquiv.symm_apply_apply]

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