rightAngleRotation_symm

Mathlib.Analysis.InnerProductSpace.TwoDim

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

← MathLib Explorer

English

J is invertible and its inverse equals minus J: J^{-1} = -J.

Русский

Обратимый оператор J, обратный ему равен −J: J^{-1} = −J.

LaTeX

$$$J^{-1} = -J$$$

Lean4

@[simp]
theorem rightAngleRotation_symm :
    LinearIsometryEquiv.symm J = LinearIsometryEquiv.trans J (LinearIsometryEquiv.neg ℝ) :=
  by
  rw [rightAngleRotation]
  exact LinearIsometryEquiv.toLinearIsometry_injective rfl

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

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

Разделы

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

Аффилиация

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