English
For A ∈ so′(p,q;R), applying the isomorphism soIndefiniteEquiv yields the conjugated matrix Pso^{-1} A Pso.
Русский
Пусть A ∈ so′(p,q;R). Применение soIndefiniteEquiv даёт конъюгированную матрицу Pso^{-1} A Pso.
LaTeX
$$$ (soIndefiniteEquiv(p,q,R,i)\,A) = (Pso(p,q,R,i))^{-1} \cdot A \cdot Pso(p,q,R,i). $$$
Lean4
/-- A matrix defining a canonical odd-rank symmetric bilinear form.
It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:
[ 2 0 0 ]
[ 0 0 1 ]
[ 0 1 0 ]
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 JB :=
Matrix.fromBlocks ((2 : R) • (1 : Matrix Unit Unit R)) 0 0 (JD l R)
