inner_rightAngleRotationAux₁_right

English

For all x, y in E, the inner product of x with the auxiliary right-angle rotation applied to y equals the negative area form: ⟨x, o.rightAngleRotationAux₁ y⟩ = -ω(x, y).

Русский

Для любых x, y ∈ E имеем: ⟨x, o.rightAngleRotationAux₁ y⟩ = -ω(x, y).

LaTeX

$$$\\\\langle x, o.rightAngleRotationAux₁ y\\\\rangle = -\\\\omega(x, y)$$$

Lean4

@[simp]
theorem inner_rightAngleRotationAux₁_right (x y : E) : ⟪x, o.rightAngleRotationAux₁ y⟫ = -ω x y :=
  by
  rw [real_inner_comm]
  simp [o.areaForm_swap y x]

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