English
The classical Lie algebra of type D is realized as the Lie subalgebra of matrices that are skew-adjoint with respect to the standard JD form; i.e., type D_l(R) consists of matrices A with A^T JD + JD A = 0.
Русский
Классическая Ли-алгебра типа D представляется как подподалгебра матриц, которые ложно-самопризнаны по отношению к форме JD; то есть JD-модуля типа D_l(R) состоит из матриц A с условием A^T JD + JD A = 0.
LaTeX
$$$\mathrm{typeD} [Fintype\ l] := \{ A \in \mathfrak{gl}_{\sum l \;\sum l}(R) \mid A^T JD_l(R) + JD_l(R) A = 0 \}$$$
Lean4
/-- The classical Lie algebra of type D as a Lie subalgebra of matrices associated to the matrix
`JD`. -/
def typeD [Fintype l] :=
skewAdjointMatricesLieSubalgebra (JD l R)
