kahler_rotation_right — Mathlib

English

Rotating the second vector scales Kahler form by the angle θ: o.kahler x (o.rotation θ y) = θ.toCircle o.kahler x y.

Русский

Поворот второго вектора на θ масштабирует Kahler форму на θ: o.kahler x (o.rotation θ y) = θ.toCircle o.kahler x y.

LaTeX

$$$ o.kahler x (o.rotation(\theta) y) = \theta.toCircle \cdot o.kahler x y $$$

Lean4

/-- Rotating the second of two vectors by `θ` scales their Kähler form by `cos θ + sin θ * I`. -/
@[simp]
theorem kahler_rotation_right (x y : V) (θ : Real.Angle) : o.kahler x (o.rotation θ y) = θ.toCircle * o.kahler x y :=
  by
  simp only [o.rotation_apply, map_add, LinearMap.map_smulₛₗ, RingHom.id_apply, real_smul,
    kahler_rightAngleRotation_right, Real.Angle.coe_toCircle]
  ring

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