mem_iff' — Mathlib

English

A matrix lies in the symplectic group iff A^T J A = J, where J is the standard symplectic form.

Русский

Матрица принадлежит симплектической группе тогда и только тогда, когда A^T J A = J, где J — стандартная симплектическая форма.

LaTeX

$$A ∈ Sp(l,R) ⇔ A^T J(l,R) A = J(l,R)$$

Lean4

theorem mem_iff' : A ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R := by
  rw [← transpose_mem_iff, mem_iff, transpose_transpose]

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