English
Same relation as Kahler Rotation Left but expressed via alternative form: o.kahler(o.rotation(θ)x, y) = (-θ).toCircle o.kahler(x, y).
Русский
То же самое, что и Kahler Rotation Left, выраженное в иной форме: o.kahler(o.rotation(θ)x, y) = (-θ).toCircle o.kahler(x, y).
LaTeX
$$$ o.kahler (o.rotation(\theta) x) y = (-\theta).toCircle \cdot o.kahler x y $$$
Lean4
/-- Rotating the first of two vectors by `θ` scales their Kähler form by `cos θ - sin θ * I`. -/
@[simp]
theorem kahler_rotation_left (x y : V) (θ : Real.Angle) :
o.kahler (o.rotation θ x) y = conj (θ.toCircle : ℂ) * o.kahler x y :=
by
simp only [o.rotation_apply, map_add, map_mul, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.add_apply,
LinearMap.smul_apply, real_smul, kahler_rightAngleRotation_left, Real.Angle.coe_toCircle, Complex.conj_ofReal,
conj_I]
ring
