areaForm_rightAngleRotation_right

Mathlib.Analysis.InnerProductSpace.TwoDim

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

← MathLib Explorer

English

Area form with second argument rotated by J equals inner product: ω(x, J y) = ⟨x, y⟩.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem areaForm_rightAngleRotation_right (x y : E) : ω x (J y) = ⟪x, y⟫ := by
  rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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