English
PD is the block matrix PD(l,R) = Matrix.fromBlocks 1 (-1) 1 1, i.e., a 2×2 block matrix with I_l in the top-left, -I_l in the bottom-right, and zero off-diagonal blocks.
Русский
PD(l,R) — блочная матрица PD(l,R) = Matrix.fromBlocks 1 (-1) 1 1, т.е. блочная матрица 2×2 с I_l в верхнем левом блоке, -I_l в нижнем правом блоке и нулевыми блоками по диагоналям и вне диагоналей.
LaTeX
$$$ PD(l,R) = \begin{pmatrix} I_l & -I_l \\ I_l & I_l \end{pmatrix},$$$
Lean4
/-- A matrix transforming the bilinear form defined by the matrix `JD` into a split-signature
diagonal matrix.
It looks like this as a `2l x 2l` matrix of `l x l` blocks:
[ 1 -1 ]
[ 1 1 ]
-/
def PD : Matrix (l ⊕ l) (l ⊕ l) R :=
Matrix.fromBlocks 1 (-1) 1 1
