Theorems · Definition · nonassociative algebras

LieAlgebra.Orthogonal.PD

(l : Type u_4) → (R : Type u₂) → [DecidableEq l] → [CommRing R] → Matrix (l ⊕ l) (l ⊕ l) R

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 ] ``

Defined in

Mathlib.Algebra.Lie.Classical

Cited by

5 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqCommRing