so — Mathlib · SciLib

English

The definite orthogonal Lie subalgebra consists of matrices skew-adjoint with respect to the identity bilinear form.

Русский

Определенная ортогональная подпалгебра Ли состоит из матриц, которые являются косо-сопряженными к форме по единичной матрице.

LaTeX

$$$$ so_n(R) = \{ X \in \mathrm{Mat}_n(R) \mid X^T + X = 0 \}. $$$$

Lean4

/-- The definite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric
bilinear form defined by the identity matrix. -/
def so [Fintype n] : LieSubalgebra R (Matrix n n R) :=
  skewAdjointMatricesLieSubalgebra (1 : Matrix n n R)

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