typeB — Mathlib

English

The classical Lie algebra of type B is the subalgebra of skew-adjoint matrices associated to the JB matrix: typeB(l,R) = skewAdjointMatricesLieSubalgebra(JB(l,R)).

Русский

Классическая Ли-алгебра типа B — подалгебра косо-сопряжённых матриц, связанных с JB: typeB(l,R) = skewAdjointMatricesLieSubalgebra(JB(l,R)).

LaTeX

$$$ typeB(l,R) = skewAdjointMatricesLieSubalgebra(JB(l,R)). $$$

Lean4

/-- The classical Lie algebra of type B as a Lie subalgebra of matrices associated to the matrix
`JB`. -/
def typeB [Fintype l] :=
  skewAdjointMatricesLieSubalgebra (JB l R)

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