JD — Mathlib · SciLib

English

The matrix JD is the canonical block matrix JD = Matrix.fromBlocks 0 1 1 0, i.e., a 2×2 block matrix with off-diagonal identity blocks and zero blocks on the diagonal.

Русский

Матрица JD является канонической блочной матрицей: JD = Matrix.fromBlocks 0 1 1 0, то есть блочно-расположенная 2×2 матрица с единичными блоками на недиагоналях и нулевыми на диагонали.

LaTeX

$$$ JD = \begin{pmatrix} 0 & I_l \\ I_l & 0 \end{pmatrix},$$$

Lean4

/-- A matrix defining a canonical even-rank symmetric bilinear form.

It looks like this as a `2l x 2l` matrix of `l x l` blocks:

   [ 0 1 ]
   [ 1 0 ]
-/
def JD : Matrix (l ⊕ l) (l ⊕ l) R :=
  Matrix.fromBlocks 0 1 1 0

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