inner_rightAngleRotation_self

Mathlib.Analysis.InnerProductSpace.TwoDim

URI: https://scilib.ai/kg/mathlib#Orientation.inner_rightAngleRotation_self

English

For all x, the inner product of J x with x is zero: ⟪J x, x⟫ = 0.

Русский

Для любого x выполнено ⟪J x, x⟫ = 0.

LaTeX

$$$\\\\langle J x, x\\\\rangle = 0$$$

Lean4

theorem inner_rightAngleRotation_self (x : E) : ⟪J x, x⟫ = 0 := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru