English
JB is the canonical odd-rank bilinear form matrix: JB = Matrix.fromBlocks (2•1) 0 0 JD, i.e., a block matrix with a 2×2 top-left block and JD in the bottom-right.
Русский
JB — каноническая матрица формы билиарной формы нечётной ранговости: JB = Matrix.fromBlocks(2)0 0 JD.
LaTeX
$$$ JB(l,R) = \begin{pmatrix} 2 & 0 \\ 0 & JD(l,R) \end{pmatrix}, $$$
Lean4
/-- A matrix transforming the bilinear form defined by the matrix `JB` into an
almost-split-signature diagonal matrix.
It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:
[ 1 0 0 ]
[ 0 1 -1 ]
[ 0 1 1 ]
where sizes of the blocks are:
[`1 x 1` `1 x l` `1 x l`]
[`l x 1` `l x l` `l x l`]
[`l x 1` `l x l` `l x l`]
-/
def PB :=
Matrix.fromBlocks (1 : Matrix Unit Unit R) 0 0 (PD l R)
