coe_inv — Mathlib

English

The inverse of a symplectic matrix, when viewed as a matrix, has the standard block form: its matrix is (-J) times the transpose of the original, times J.

Русский

Обратная симплектической матрицы, рассматриваемая как матрица, имеет стандартную блочную форму: её матрица равна (-J) умноженному на транспонированную матрицу A и снова на J.

LaTeX

$$$\\uparrow A^{-1} = (-J) A^T J$$$

Lean4

theorem coe_inv (A : symplecticGroup l R) : (↑A⁻¹ : Matrix _ _ _) = (-J l R) * (↑A)ᵀ * J l R :=
  rfl

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