skewAdjointMatricesLieSubalgebra — Mathlib

English

The Lie subalgebra of skew-adjoint square matrices associated to J consists of those matrices which are skew-adjoint with respect to J.

Русский

Ли-подалгебра кососопряжённых квадратных матриц, связанных с J, состоит из матриц, которые кососопряжены по отношению к J.

LaTeX

$$\text{The LieSubalgebra of skew-adjoint matrices is associated to } J.$$

Lean4

/-- The Lie subalgebra of skew-adjoint square matrices corresponding to a square matrix `J`. -/
def skewAdjointMatricesLieSubalgebra : LieSubalgebra R (Matrix n n R) :=
  { skewAdjointMatricesSubmodule J with lie_mem' := J.isSkewAdjoint_bracket }

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