English
The skew-adjoint endomorphisms of a module M, with respect to a bilinear form B, form a Lie subalgebra of the Lie algebra of all endomorphisms of M.
Русский
Кососопряжённые эндоморфизмы модуля M по отношению к билинейной форме B образуют Ли-подалгебру над всем множеством эндоморфизмов M.
LaTeX
$$\text{The set of skew-adjoint endomorphisms with respect to } B \text{ forms a LieSubalgebra of } \mathrm{End}_R(M).$$
Lean4
/-- Given an `R`-module `M`, equipped with a bilinear form, the skew-adjoint endomorphisms form a
Lie subalgebra of the Lie algebra of endomorphisms. -/
def skewAdjointLieSubalgebra : LieSubalgebra R (Module.End R M) :=
{ B.skewAdjointSubmodule with lie_mem' := B.isSkewAdjoint_bracket }
