English
The symplectic group consists of all A in the full matrix ring M_{(l⊕l)×(l⊕l)}(R) such that A J A^T = J, i.e., those preserving the canonical skew form.
Русский
Группа симплексных матриц состоит из всех A в полной матричной алгебре, удовлетворяющих A J A^T = J, то есть сохраняющих каноническую кососимметрическую форму.
LaTeX
$$$\operatorname{symplecticGroup}(l,R) = \{ A \in M_{(l\oplus l)\times(l\oplus l)}(R) \mid A J(l,R) A^T = J(l,R) \}$$$
Lean4
/-- The group of symplectic matrices over a ring `R`. -/
def symplecticGroup : Submonoid (Matrix (l ⊕ l) (l ⊕ l) R)
where
carrier := {A | A * J l R * Aᵀ = J l R}
mul_mem' {a b} ha
hb := by
simp only [Set.mem_setOf_eq, transpose_mul] at *
rw [← Matrix.mul_assoc, a.mul_assoc, a.mul_assoc, hb]
exact ha
one_mem' := by simp
