kahler_rotation_left' — Mathlib

English

Negating rotation by π/2 equals rotation by -π/2 (alternative form).

Русский

Отрицание вращения на π/2 эквивалентно вращению на -π/2 (альтернативная форма).

LaTeX

$$$\text{neg_rotation_pi_div_two} = \text{neg_rotation_neg_pi_div_two}$$$

Lean4

/-- Rotating the first of two vectors by `θ` scales their Kähler form by `cos (-θ) + sin (-θ) * I`.
-/
theorem kahler_rotation_left' (x y : V) (θ : Real.Angle) : o.kahler (o.rotation θ x) y = (-θ).toCircle * o.kahler x y :=
  by simp only [Real.Angle.toCircle_neg, Circle.coe_inv_eq_conj, kahler_rotation_left]

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