inv_eq_symplectic_inv — Mathlib

English

For any A and hA ∈ Sp, the inverse equals the explicit symplectic expression: A^{-1} = (-J) A^T J.

Русский

Для любой A с hA ∈ Sp, обратная матрица задаётся явной симплексной формулой: A^{-1} = (-J) A^T J.

LaTeX

$$A^{-1} = (-J(l,R)) * A^T * J(l,R)$$

Lean4

theorem inv_eq_symplectic_inv (A : Matrix (l ⊕ l) (l ⊕ l) R) (hA : A ∈ symplecticGroup l R) :
    A⁻¹ = (-J l R) * Aᵀ * J l R :=
  inv_eq_left_inv (by simp only [Matrix.neg_mul, inv_left_mul_aux hA])

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