rotation_map_complex — Mathlib

English

There is compatibility between orientation rotation and complex scalar multiplication via a linear isometry to C.

Русский

Сопоставление ориентации и вращения согласуется с умножением на комплексное число через линейное изоморфизмированное отображение.

LaTeX

$$f (o.rotation θ x) = θ.toCircle · f x$$

Lean4

/-- Rotation in an oriented real inner product space of dimension 2 can be evaluated in terms of a
complex-number representation of the space. -/
theorem rotation_map_complex (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x : V) :
    f (o.rotation θ x) = θ.toCircle * f x := by
  rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]

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