kahler_rightAngleRotation_left — Mathlib

English

Replacing the first argument by Jx multiplies kahler by −i: kahler(Jx, y) = −i kahler(x,y).

Русский

Замена первого аргумента на Jx умножает kahler на −i: kahler(Jx,y) = −i kahler(x,y).

LaTeX

$$kahler\\_rightAngleRotation\\_left (x,y) : o.kahler (J x) y = -i \\; o.kahler x y$$

Lean4

@[simp]
theorem kahler_rightAngleRotation_left (x y : E) : o.kahler (J x) y = -Complex.I * o.kahler x y :=
  by
  simp only [o.areaForm_rightAngleRotation_left, o.inner_rightAngleRotation_left, o.kahler_apply_apply,
    Complex.ofReal_neg, Complex.real_smul]
  linear_combination ω x y * Complex.I_sq

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