Theorems · Theorem · nonassociative algebras

LieAlgebra.Orthogonal.indefiniteDiagonal_assoc

∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  LieAlgebra.Orthogonal.indefiniteDiagonal (Unit ⊕ l) l R =
    (Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm)
      (Matrix.fromBlocks 1 0 0 (LieAlgebra.Orthogonal.indefiniteDiagonal l l R))

Defined in

Mathlib.Algebra.Lie.Classical

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommRingFintype