inner_rightAngleRotation_swap' — Mathlib

English

A variant of the skew-symmetry: ⟪J x, y⟫ = −⟪x, J y⟫ is equivalent to ⟪x, J y⟫ = −⟪J x, y⟫.

Русский

Вариант кососимметрии: эквивалентно ⟪J x, y⟫ = −⟪x, J y⟫ равно ⟪x, J y⟫ = −⟪J x, y⟫.

LaTeX

$$$\\\\langle J x, y\\\\rangle = -\\\\langle x, J y\\\\rangle$$$

Lean4

theorem inner_rightAngleRotation_swap' (x y : E) : ⟪J x, y⟫ = -⟪x, J y⟫ := by simp [o.inner_rightAngleRotation_swap x y]

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