hasInv — Mathlib

English

The symplectic group is a group under multiplication; for A ∈ Sp, A^{-1} is given by a concrete formula in terms of J and A^T:

Русский

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

LaTeX

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

Lean4

instance hasInv : Inv (symplecticGroup l R) where
  inv
    A :=
    ⟨(-J l R) * (A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R,
      mul_mem (mul_mem (neg_mem <| J_mem _ _) <| transpose_mem A.2) <| J_mem _ _⟩

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