mem_iff

Mathlib.LinearAlgebra.SymplecticGroup

URI: https://scilib.ai/kg/mathlib#SymplecticGroup.mem_iff

English

A belongs to the symplectic group if and only if A J A^T = J.

Русский

Элемент A принадлежит группе симплексных тогда и только тогда, когда A J A^T = J.

LaTeX

$$$A \in \operatorname{symplecticGroup}(l,R) \;\Leftrightarrow\; A J(l,R) A^T = J(l,R)$$$

Lean4

theorem mem_iff {A : Matrix (l ⊕ l) (l ⊕ l) R} : A ∈ symplecticGroup l R ↔ A * J l R * Aᵀ = J l R := by
  simp [symplecticGroup]

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

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

Разделы

Аффилиация

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