J_transpose

Mathlib.LinearAlgebra.SymplecticGroup

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

← MathLib Explorer

English

The transpose of J is the negative of J: J^T = -J.

Русский

Транспонированная матрица J равна противоположной J: J^T = -J.

LaTeX

$$$J^{\top} = -J$$$

Lean4

@[simp]
theorem J_transpose : (J l R)ᵀ = -J l R :=
  by
  rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R), fromBlocks_smul,
    Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]
  simp [fromBlocks]

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

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

Разделы

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

Аффилиация

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