J_squared

Mathlib.LinearAlgebra.SymplecticGroup

URI: https://scilib.ai/kg/mathlib#Matrix.J_squared

← MathLib Explorer

English

The inverse of J is minus J: J^{-1} = -J.

Русский

Обратная матрица J равна -J: J^{-1} = -J.

LaTeX

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

Lean4

theorem J_squared : J l R * J l R = -1 := by
  rw [J, fromBlocks_multiply]
  simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]
  rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]

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

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

Разделы

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

Аффилиация

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