so' — Mathlib

English

A matrix Pso(p,q,R,i) is the diagonal matrix with entries 1 on the p-block and i on the q-block on the diagonal.

Русский

Матрица Pso(p,q,R,i) диагональная: на первом блоке p единиц, на втором блоке q значение i на диагонали.

LaTeX

$$$$ Pso(p,q,R,i) = \operatorname{diag}( \underbrace{1,\dots,1}_{p}, \underbrace{i,\dots,i}_{q} ). $$$$

Lean4

/-- The indefinite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric
bilinear form defined by the indefinite diagonal matrix. -/
def so' [Fintype p] [Fintype q] : LieSubalgebra R (Matrix (p ⊕ q) (p ⊕ q) R) :=
  skewAdjointMatricesLieSubalgebra <| indefiniteDiagonal p q R

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