kahler_comp_rightAngleRotation'

Mathlib.Analysis.InnerProductSpace.TwoDim

URI: https://scilib.ai/kg/mathlib#Orientation.kahler_comp_rightAngleRotation'

← MathLib Explorer

English

A variant form of invariance under a square of i: −i(i kahler(x,y)) = kahler(x,y).

Русский

Вариант инвариантности под i: −i(i kahler(x,y)) = kahler(x,y).

LaTeX

$$−i (i o.kahler x y) = o.kahler x y$$

Lean4

theorem kahler_comp_rightAngleRotation' (x y : E) : -(Complex.I * (Complex.I * o.kahler x y)) = o.kahler x y := by
  linear_combination -o.kahler x y * Complex.I_sq

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

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

Разделы

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

Аффилиация

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