areaForm_rightAngleRotation_left — Mathlib

English

Area form after applying J to the first argument equals minus the inner product: ω(J x, y) = −⟨x, y⟩.

Русский

Площадная форма после применения J к первому аргументу равна минус скалярному произведению: ω(J x, y) = −⟨x, y⟩.

LaTeX

$$$\\\\omega(J x, y) = -\\\\langle x, y\\\\rangle$$$

Lean4

@[simp]
theorem areaForm_rightAngleRotation_left (x y : E) : ω (J x) y = -⟪x, y⟫ := by
  rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]

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