kahler_rightAngleRotation_right — Mathlib

English

Replacing the second argument by Jz multiplies kahler by i: kahler(x, Jy) = i kahler(x,y).

Русский

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

LaTeX

$$kahler\\_rightAngleRotation\\_right (x,y) : o.kahler x (J y) = i o.kahler x y$$

Lean4

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

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